isUnitSubmonoid_eq_nonZeroDivisorsRight

English

In an Artinian ring, the unit submonoid equals the right non-zero divisors.

Русский

В артиновом кольце единицы совпадают с правыми не нулевыми делителями.

LaTeX

$$$\mathrm{IsUnit.submonoid}(R) = \mathrm{NZD}_{\text{right}}(R)$$$

Lean4

theorem isUnitSubmonoid_eq_nonZeroDivisorsRight [IsArtinianRing R] : IsUnit.submonoid R = nonZeroDivisorsRight R := by
  ext; rw [← isRightRegular_iff_mem_nonZeroDivisorsRight]; exact isUnit_iff_isRightRegular

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