isUnit_iff_mem_nonZeroDivisors_of_mulOpposite

English

In an Artinian ring, a is a unit iff a ∈ R⁰ (non-zero-divisors).

Русский

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

LaTeX

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

Lean4

theorem isUnit_iff_mem_nonZeroDivisors_of_mulOpposite [IsArtinianRing Rᵐᵒᵖ] {a : R} : IsUnit a ↔ a ∈ R⁰ := by
  rw [isUnit_iff_isRegular_of_mulOpposite, isRegular_iff_mem_nonZeroDivisors]

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