eq_iff_smodEq — Mathlib

English

If IsHausdorff (⊤ : Ideal R) M holds, then M is a singleton.

Русский

Если IsHausdorff (⊤) M, тогда M одноэлементно.

LaTeX

$$$\text{If } IsHausdorff(\top)\ M, \text{ then } M \text{ is Subsingleton}$$$

Lean4

theorem eq_iff_smodEq [IsHausdorff I M] {x y : M} : x = y ↔ ∀ n, x ≡ y [SMOD (I ^ n • ⊤ : Submodule R M)] :=
  by
  refine ⟨fun h _ ↦ h ▸ rfl, fun h ↦ ?_⟩
  rw [← sub_eq_zero]
  apply IsHausdorff.haus' (I := I) (x - y)
  simpa [SModEq.sub_mem] using h

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