isUnit_iff_nonZeroDivisor_of_isIntegral'

English

In an algebra with IsIntegral, a is a unit iff a is not a zero divisor.

Русский

В алгебре с условием интегрированности элемент a является единицей тогда и только тогда, когда он не является нулевым делителем.

LaTeX

$$$[\\text{Algebra.IsIntegral } R A] \\;\\Rightarrow\\; (\\mathrm{IsUnit}(a) \\iff a \\in A^0)$$$

Lean4

/-- Integral element of an algebra over Artinian ring `R` is either a zero divisor or a unit. -/
theorem isUnit_iff_nonZeroDivisor_of_isIntegral' [Algebra.IsIntegral R A] {a : A} : IsUnit a ↔ a ∈ A⁰ :=
  isUnit_iff_nonZeroDivisor_of_isIntegral (R := R) (Algebra.IsIntegral.isIntegral a)

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