isUnit_iff_isRegular — Mathlib

English

Let R be an Artinian ring (in particular a semiring with Artinian property). Then for every x ∈ R, x is a unit if and only if x is regular (i.e., not a zero-divisor). In particular, in Artinian rings, units coincide with regular elements.

Русский

Пусть R — артиново кольцо. Тогда для любого x ∈ R элемент является единицей тогда и только тогда, когда он регулярный (то есть не является нулевым делителем). В частности, в артиновых кольцах единицы совпадают с регулярными элементами.

LaTeX

$$$\mathrm{IsUnit}(x) \iff \mathrm{IsRegular}(x)$$$

Lean4

theorem isUnit_iff_isRegular [IsArtinianRing R] {x : R} : IsUnit x ↔ IsRegular x := by
  rw [isRegular_iff, ← isUnit_iff_isRightRegular, and_iff_right_of_imp (·.isRegular.1)]

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