zero_iff_subsingleton — Mathlib

English

The element 0 is M-regular if and only if M is trivial.

Русский

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

LaTeX

$$$IsSMulRegular M 0 \iff Subsingleton M$$$

Lean4

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

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