subsingleton_quotient_iff_eq_top — Mathlib

English

The quotient M / p is a Subsingleton (i.e., has at most one element) if and only if p = ⊤.

Русский

Фактор-модуль M / p является одноместным тогда и только тогда, когда p = ⊤.

LaTeX

$$$$ \\operatorname{Subsingleton}(M / p) \\;\\Longleftrightarrow\\; p = \\top. $$$$

Lean4

theorem subsingleton_quotient_iff_eq_top : Subsingleton (M ⧸ p) ↔ p = ⊤ :=
  by
  constructor
  · rintro h
    refine eq_top_iff.mpr fun x _ => ?_
    have : x - 0 ∈ p := (Submodule.Quotient.eq p).mp (Subsingleton.elim _ _)
    rwa [sub_zero] at this
  · rintro rfl
    infer_instance

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