subsingleton — Mathlib

English

If the adic completion with respect to the top ideal is complete, then the underlying module M is a singleton.

Русский

Если адическое завершение по топ-идеалу полное, то исходный модуль M тождественно единичен.

LaTeX

$$$\text{IsAdicComplete}(\top : \text{Ideal } R)\ M \Rightarrow \operatorname{Subsingleton} M$$$

Lean4

protected theorem subsingleton (h : IsAdicComplete (⊤ : Ideal R) M) : Subsingleton M :=
  h.1.subsingleton

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