Quotient_Mapping_on_Structure_is_Canonical_Epimorphism
Provedepimorphismsproofwikiquotient-structures
The quotient mapping from a group to its quotient by a normal subgroup is a surjective homomorphism.
Preamble
import Mathlib.GroupTheory.QuotientGroup.Basic
Formal statement
theorem Quotient_Mapping_on_Structure_is_Canonical_Epimorphism {G : Type _} [Group G] (N : Subgroup G) [N.Normal] : Function.Surjective (QuotientGroup.mk' N) := by sorrySource