isLeftRegular_zero_iff_subsingleton

English

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

Русский

Пусть R является структурой MulZeroClass. Тогда элемент 0 слева регулярный тогда и только тогда, когда R тривиален (обладает единственным элементом).

LaTeX

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

Lean4

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

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