isRightRegular_zero_iff_subsingleton

English

Let R be a MulZeroClass. Then the element 0 is right-regular if and only if R is a trivial (subsingleton) ring.

Русский

Пусть R является MulZeroClass. Тогда ноль справа-регулярен тогда и только тогда, когда R тривиален.

LaTeX

$$$IsRightRegular(0) \iff \operatorname{Subsingleton}(R)$$$

Lean4

/-- The element `0` is right-regular if and only if `R` is trivial. -/
theorem isRightRegular_zero_iff_subsingleton : IsRightRegular (0 : R) ↔ Subsingleton R :=
  ⟨fun h => h.subsingleton, fun H a b _ => @Subsingleton.elim _ H a b⟩

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