# Documentation

Mathlib.LinearAlgebra.TensorProductBasis

# Bases and dimensionality of tensor products of modules #

These can not go into LinearAlgebra.TensorProduct since they depend on LinearAlgebra.FinsuppVectorSpace which in turn imports LinearAlgebra.TensorProduct.

def Basis.tensorProduct {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} {κ : Type u_5} [] [] [Module R M] [] [Module R N] (b : Basis ι R M) (c : Basis κ R N) :
Basis (ι × κ) R ()

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

Instances For
@[simp]
theorem Basis.tensorProduct_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} {κ : Type u_5} [] [] [Module R M] [] [Module R N] (b : Basis ι R M) (c : Basis κ R N) (i : ι) (j : κ) :
↑() (i, j) = b i ⊗ₜ[R] c j
theorem Basis.tensorProduct_apply' {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} {κ : Type u_5} [] [] [Module R M] [] [Module R N] (b : Basis ι R M) (c : Basis κ R N) (i : ι × κ) :
↑() i = b i.fst ⊗ₜ[R] c i.snd
@[simp]
theorem Basis.tensorProduct_repr_tmul_apply {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} {κ : Type u_5} [] [] [Module R M] [] [Module R N] (b : Basis ι R M) (c : Basis κ R N) (m : M) (n : N) (i : ι) (j : κ) :
↑(().repr (m ⊗ₜ[R] n)) (i, j) = ↑(b.repr m) i * ↑(c.repr n) j