Quotient_Theorem_for_Epimorphisms
Provedepimorphismsproofwikiquotient-structures
If f: G → H is a surjective group homomorphism, then G/ker(f) is isomorphic to H.
Preamble
import Mathlib.GroupTheory.QuotientGroup.Basic
Formal statement
theorem Quotient_Theorem_for_Epimorphisms {G H : Type _} [Group G] [Group H] (f : G →* H) (hsurj : Function.Surjective f) : Nonempty (G ⧸ f.ker ≃* H) := by sorrySource