instNoZeroDivisors — Mathlib

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

Похожие утверждения