English
If R has no zero divisors and M is a free R-module, then TensorAlgebra R M has no zero divisors.
Русский
Если в кольце R нет нулевых делителей и M является свободным модулем над R, то у TensorAlgebra R M нет нулевых делителей.
LaTeX
$$$ NoZeroDivisors (TensorAlgebra R M) $$$
Lean4
/-- The `TensorAlgebra` of a free module over a commutative semiring with no zero-divisors has
no zero-divisors. -/
instance instNoZeroDivisors [NoZeroDivisors R] [Module.Free R M] : NoZeroDivisors (TensorAlgebra R M) :=
have ⟨⟨_, b⟩⟩ := ‹Module.Free R M›
(equivFreeAlgebra b).toMulEquiv.noZeroDivisors