isRegular_iff_subsingleton — Mathlib

English

The element 0 is regular if and only if R is subsingleton.

Русский

Элемент 0 регулярен тогда и только тогда, когда R является subsingleton.

LaTeX

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

Lean4

/-- The element `0` is regular if and only if `R` is trivial. -/
theorem isRegular_iff_subsingleton : IsRegular (0 : R) ↔ Subsingleton R :=
  ⟨fun h => h.left.subsingleton, fun h =>
    ⟨isLeftRegular_zero_iff_subsingleton.mpr h, isRightRegular_zero_iff_subsingleton.mpr h⟩⟩

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