instNoZeroDivisors — Mathlib

English

If R has no zero divisors, then FreeAlgebra R X has no zero divisors as well.

Русский

Если у R нет делителей нуля, то у FreeAlgebra R X тоже нет делителей нуля.

LaTeX

$$$\text{NoZeroDivisors } R \Rightarrow \text{NoZeroDivisors } \mathrm{FreeAlgebra}(R,X)$$$

Lean4

/-- `FreeAlgebra R X` has no zero-divisors when `R` has no zero-divisors. -/
instance instNoZeroDivisors [NoZeroDivisors R] : NoZeroDivisors (FreeAlgebra R X) :=
  equivMonoidAlgebraFreeMonoid.toMulEquiv.noZeroDivisors

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