isUnit_iff_mem_nonZeroDivisors — Mathlib

English

In an Artinian ring, an element is a unit iff it is a non-zero-divisor.

Русский

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

LaTeX

$$$\mathrm{IsUnit}(a) \iff a \in \mathrm{NZD}(R)$$$

Lean4

/-- In an Artinian ring, an element is a unit iff it is a non-zero-divisor.
See also `isUnit_iff_mem_nonZeroDivisors_of_finite`. -/
theorem isUnit_iff_mem_nonZeroDivisors [IsArtinianRing R] {a : R} : IsUnit a ↔ a ∈ R⁰ := by
  rw [isUnit_iff_isRegular, isRegular_iff_mem_nonZeroDivisors]

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