Products of TensorAlgebra.tprod

TensorAlgebra.tprod_mul_tprod multiplies two products of generators by appending their factors, and TensorAlgebra.span_tprod_eq_top says these products span the tensor algebra, with the linear induction principle TensorAlgebra.induction_tprod. They are the tensor algebra siblings of ExteriorAlgebra.ιMulti_mul_ιMulti and ExteriorAlgebra.ιMulti_span. [UPSTREAM] All belong in Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean.

theorem TensorAlgebra.tprod_mul_tprod {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {m n : ℕ} (a : Fin m → M) (b : Fin n → M) : (tprod R M m) a * (tprod R M n) b = (tprod R M (m + n)) (Fin.append a b)

theorem TensorAlgebra.span_tprod_eq_top (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] : Submodule.span R (⋃ (n : ℕ), Set.range ⇑(tprod R M n)) = ⊤

The products tprod R M n x of generators span the tensor algebra.

theorem TensorAlgebra.induction_tprod {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {motive : TensorAlgebra R M → Prop} (tprod : ∀ (n : ℕ) (x : Fin n → M), motive ((tprod R M n) x)) (smul : ∀ (r : R) (a : TensorAlgebra R M), motive a → motive (r • a)) (add : ∀ (a b : TensorAlgebra R M), motive a → motive b → motive (a + b)) (a : TensorAlgebra R M) : motive a