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.ι_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