isUnit_iff_isRegular_of_mulOpposite

English

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

Русский

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

LaTeX

$$$a \in \mathrm{NZD}(R) \implies \mathrm{IsUnit}(a)\quad (R\text{ Artinian})$$$

Lean4

theorem isUnit_iff_isRegular_of_mulOpposite [IsArtinianRing Rᵐᵒᵖ] {x : R} : IsUnit x ↔ IsRegular x := by
  rw [isRegular_iff, ← isUnit_iff_isLeftRegular, and_iff_left_of_imp (·.isRegular.2)]

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