Theorems · Definition · group theory

QuotientAddGroup.congr

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

QuotientAddGroup.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

4 results in Mathlib

Foundations

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

Assumes

AddGroupAddGroupAddSubgroup.NormalAddSubgroup.Normal