unique — Mathlib

English

The quotient of M by the top submodule ⊤ is a unique (singleton) object (the zero module).

Русский

Фактор-модуль M / ⊤ является единственным объектом (одиночным модулем нуля).

LaTeX

$$$$ M / \\top \\cong \\{0\\} \\quad\\text{(a singleton).} $$$$

Lean4

instance unique : Unique (M ⧸ (⊤ : Submodule R M))
    where
  default := 0
  uniq x := Submodule.Quotient.induction_on _ x fun _x => (Submodule.Quotient.eq ⊤).mpr Submodule.mem_top

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