mk'_surjective — Mathlib

English

The natural quotient map c.mk' is surjective.

Русский

Естественное отображение-квартирование c.mk' сюръективно.

LaTeX

$$$Surjective\; c.mk' $$$

Lean4

/-- The natural homomorphism from a monoid to its quotient by a congruence relation is
surjective. -/
@[to_additive /-- The natural homomorphism from an `AddMonoid` to its quotient by a congruence
    relation is surjective. -/
    ]
theorem mk'_surjective : Surjective c.mk' :=
  Quotient.mk''_surjective

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