isUnit_submonoid_eq_of_isIntegral

English

If Algebra.IsIntegral holds, the unit submonoid equals the non-zero divisors submonoid.

Русский

Если выполняется интегральность, то подмонойд единиц равен подмонойду не нулевых делителей.

LaTeX

$$$[Algebra.IsIntegral R A] \\Rightarrow \\mathrm{IsUnit.submonoid} A = A^0$$$

Lean4

theorem isUnit_submonoid_eq_of_isIntegral [Algebra.IsIntegral R A] : IsUnit.submonoid A = A⁰ := by ext;
  simpa [IsUnit.mem_submonoid_iff] using isUnit_iff_nonZeroDivisor_of_isIntegral' (R := R)

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