instZeroQuotient — Mathlib

English

The quotient M/p is a singleton iff every x ∈ M lies in p.

Русский

Фактор-модуль M/p тождественен одному элементу тогда, когда каждый элемент M принадлежит p.

LaTeX

$$$\text{Subsingleton}(M/p) \iff \forall x\in M,\; x\in p.$$$

Lean4

instance : Zero (M ⧸ p) where
  -- Use Quotient.mk'' instead of mk here because mk is not reducible.
    -- This would lead to non-defeq diamonds.
    -- See also the same comment at the One instance for Con.
  zero := Quotient.mk'' 0

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