Theorems · Definition · group theory

Con.comapQuotientEquivOfSurj

{M : Type u_1} →
  {N : Type u_2} →
    [inst : MulOneClass M] →
      [inst_1 : MulOneClass N] →
        (c : Con M) → (f : N →* M) → Function.Surjective ⇑f → (Con.comap ⇑f ⋯ c).Quotient ≃* c.Quotient

If e : M →* N is surjective then (c.comap e).Quotient ≃* c.Quotient with c : Con N

Defined in

Mathlib.GroupTheory.Congruence.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

MulOneClassMulOneClass