Theorems · Definition · group theory

QuotientGroup.congr

{G : Type u_1} →
  {H : Type u_2} →
    [inst : Group G] →
      [inst_1 : Group H] →
        (G' : Subgroup G) →
          (H' : Subgroup H) →
            [inst_2 : G'.Normal] → [inst_3 : H'.Normal] → (e : G ≃* H) → Subgroup.map (↑e) G' = H' → G ⧸ G' ≃* H ⧸ H'

QuotientGroup.congr lifts the isomorphism e : G ≃ H to G ⧸ G' ≃ H ⧸ H', given that e maps G to H.

Defined in

Mathlib.GroupTheory.QuotientGroup.Defs

Cited by

16 results in Mathlib

Foundations

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

Assumes

GroupGroupSubgroup.NormalSubgroup.Normal