Theorems · Definition · group theory

QuotientGroup.quotientKerEquivOfSurjective

{G : Type u} →
  [inst : Group G] → {H : Type v} → [inst_1 : Group H] → (φ : G →* H) → Function.Surjective ⇑φ → G ⧸ φ.ker ≃* H

The canonical isomorphism G/(ker φ) ≃* H induced by a surjection φ : G →* H. For a computable version, see QuotientGroup.quotientKerEquivOfRightInverse.

Defined in

Mathlib.GroupTheory.QuotientGroup.Basic

Cited by

2 results in Mathlib

Foundations

Depth 84 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

GroupGroup