Theorems · Definition · group theory

Con.quotientKerEquivOfRightInverse

{M : Type u_1} →
  {P : Type u_3} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass P] → (f : M →* P) → (g : P → M) → Function.RightInverse g ⇑f → (Con.ker f).Quotient ≃* P

The first isomorphism theorem for monoids in the case of a homomorphism with right inverse.

Defined in

Mathlib.GroupTheory.Congruence.Basic

Cited by

2 results in Mathlib

Foundations

Depth 20 from the axioms · uses propext, Quot.sound

Assumes

MulOneClassMulOneClass