subsingleton — Mathlib

English

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

Русский

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

LaTeX

$$$IsSMulRegular M 0 \Leftrightarrow Subsingleton M$$$

Lean4

/-- The element `0` is `M`-regular if and only if `M` is trivial. -/
protected theorem subsingleton (h : IsSMulRegular M (0 : R)) : Subsingleton M :=
  ⟨fun a b => h (by dsimp only [Function.comp_def]; repeat' rw [MulActionWithZero.zero_smul])⟩

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