mathlibdocumentation

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.

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] [ M] [ N] (b : R M) (c : 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
@[instance]
def finite_dimensional_tensor_product {K : Type u_1} (V : Type u_2) (W : Type u_3) [field K] [ V] [ W] [ V] [ W] :
(V W)

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