theorem TensorAlgebra.hom_ext_tprod {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] (f g : TensorAlgebra R M →ₗ[R] N) (h : ∀ (n : ℕ) (x : Fin n → M), f ((tprod R M n) x) = g ((tprod R M n) x)) : f = g

theorem TensorAlgebra.hom_ext_tprod_iff {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {N : Type u_3} [AddCommMonoid N] [Module R N] {f g : TensorAlgebra R M →ₗ[R] N} : f = g ↔ ∀ (n : ℕ) (x : Fin n → M), f ((tprod R M n) x) = g ((tprod R M n) x)

@[simp]

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

theorem TensorAlgebra.ι_mul_tprod {R : Type u_1} [CommSemiring R] {M : Type u_2} [AddCommMonoid M] [Module R M] {n : ℕ} (m : M) (x : Fin n → M) : (ι R) m * (tprod R M n) x = (tprod R M (n + 1)) (Fin.cons m x)

theorem TensorAlgebra.ι_range_pow_eq (R : Type u_1) [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] (n : ℕ) : (ι R).range ^ n = TensorPower.toTensorAlgebra.range

theorem TensorAlgebra.span_tprod_eq_top (R : Type u_1) [CommSemiring R] (M : Type u_2) [AddCommMonoid M] [Module R M] : Submodule.span R {x : TensorAlgebra R M | ∃ (n : ℕ) (f : Fin n → M), x = (tprod R M n) f} = ⊤