Theorems · Definition · group theory

QuotientAddGroup.quotientKerEquivOfRightInverse

{G : Type u} →
  [inst : AddGroup G] →
    {H : Type v} → [inst_1 : AddGroup H] → (φ : G →+ H) → (ψ : H → G) → Function.RightInverse ψ ⇑φ → G ⧸ φ.ker ≃+ H

The canonical isomorphism G/(ker φ) ≃+ H induced by a homomorphism φ : G →+ H with a right inverse ψ : H → G.

Defined in

Mathlib.GroupTheory.QuotientGroup.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddGroupAddGroup