English
The submodule lattice of M is subsingleton if and only if M is subsingleton; i.e., M has at most one element if and only if Submodule R M has at most one element.
Русский
Перестановочная подрешётка подмодулей равна нуль-единичной, если и только M — нуль-единичный; то есть векторное пространство (модуль) имеет не более одного элемента тогда и только тогда множество подмодулей имеет не более одного элемента.
LaTeX
$$$\\text{Subsingleton}(\\text{Submodule } R M) \\iff \\text{Subsingleton}(M)$$$
Lean4
@[simp]
theorem subsingleton_iff : Subsingleton (Submodule R M) ↔ Subsingleton M :=
have h : Subsingleton (Submodule R M) ↔ Subsingleton (AddSubmonoid M) := by
rw [← subsingleton_iff_bot_eq_top, ← subsingleton_iff_bot_eq_top, ← toAddSubmonoid_inj, bot_toAddSubmonoid,
top_toAddSubmonoid]
h.trans AddSubmonoid.subsingleton_iff
