← all areas

Namespace TensorProduct 8 theorems

— 7 · AlgebraTensorModule 1

directly in TensorProduct 7

• Joint zeros in a double base change lie in the span of unit tensors TensorProduct.mem_span_unitTmul_of_forall_apply_eq_zero 0 below · cited by 1 · depth 18
• Dévissage: field case implies finitely generated case TensorProduct.eq_zero_of_forall_lTensor_eq_zero_of_field 0 below · cited by 2 · depth 20
• Clearing denominators in ℚ_q ⊗_{ℤ_q} T TensorProduct.exists_pow_smul_eq_one_tmul 0 below · cited by 1 · depth 23
• Multiplication is bijective on the diagonal of K ⊗_F P TensorProduct.mulMap_injOn_and_surjOn_diagonal_of_isSeparable 0 below · cited by 1 · depth 25
• Base change isomorphism onto the K-span of an 𝔽ₚ-linear map TensorProduct.exists_linearEquiv_span_range_apply_tmul_of_natCard_eq_pow_finrank 0 below · cited by 1 · depth 29
• Transporting a tensor product along a field isomorphism TensorProduct.exists_linearEquiv_compHom_ringEquiv_tmul 0 below · cited by 1 · depth 30
• Base change along C = A ⊗_k B identifies P ⊗_k Q TensorProduct.exists_addEquiv_baseChange_tensor_baseChange_tmul_eq_of_bijective 0 below · cited by 1 · depth 36

TensorProduct.AlgebraTensorModule 1

• Cancellation of iterated base change is natural in endomorphisms TensorProduct.AlgebraTensorModule.cancelBaseChange_baseChange_baseChange_apply 0 below · cited by 1 · depth 24