Quotient_Theorem_for_Group_Epimorphisms
Provedgroup-homomorphismsisomorphism-theoremsproofwikiquotient-groups
Let φ : G → H be a group epimorphism. Then there exists a unique group isomorphism ψ : G/ker(φ) → H satisfying ψ ∘ q = φ where q is the quotient map.
Preamble
import Mathlib.GroupTheory.QuotientGroup.Basic
Formal statement
theorem Quotient_Theorem_for_Group_Epimorphisms {G H : Type _} [Group G] [Group H] (φ : G →* H) (hsurj : Function.Surjective φ) : Nonempty (G ⧸ φ.ker ≃* H) := by sorrySource