mathlib documentation

linear_algebra.tensor_product_basis

Bases and dimensionality of tensor products of modules #

These can not go into linear_algebra.tensor_product since they depend on linear_algebra.finsupp_vector_space which in turn imports linear_algebra.tensor_product.

noncomputable def basis.tensor_product {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} {κ : Type u_5} [comm_ring R] [add_comm_group M] [module R M] [add_comm_group N] [module R N] (b : basis ι R M) (c : basis κ R N) :
basis × κ) R (M N)

If b : ι → M and c : κ → N are bases then so is λ i, b i.1 ⊗ₜ c i.2 : ι × κ → M ⊗ N.

Equations
@[simp]
theorem basis.tensor_product_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} {κ : Type u_5} [comm_ring R] [add_comm_group M] [module R M] [add_comm_group N] [module R N] (b : basis ι R M) (c : basis κ R N) (i : ι) (j : κ) :
(b.tensor_product c) (i, j) = b i ⊗ₜ[R] c j
theorem basis.tensor_product_apply' {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} {κ : Type u_5} [comm_ring R] [add_comm_group M] [module R M] [add_comm_group N] [module R N] (b : basis ι R M) (c : basis κ R N) (i : ι × κ) :
@[protected, instance]
def finite_dimensional_tensor_product {K : Type u_1} (V : Type u_2) (W : Type u_3) [field K] [add_comm_group V] [module K V] [add_comm_group W] [module K W] [finite_dimensional K V] [finite_dimensional K W] :

If V and W are finite dimensional K vector spaces, so is V ⊗ W.