Theorems · Definition · group theory

QuotientAddGroup.prodAddEquiv

{G : Type u} →
  [inst : AddGroup G] →
    {H : Type v} →
      [inst_1 : AddGroup H] →
        (A : AddSubgroup G) →
          (B : AddSubgroup H) → [inst_2 : A.Normal] → [inst_3 : B.Normal] → (G × H) ⧸ A.prod B ≃+ (G ⧸ A) × H ⧸ B

(G × H) / (A × B) is isomorphic to G / A × H / B.

Defined in

Mathlib.GroupTheory.QuotientGroup.Basic

Cited by

2 results in Mathlib

Foundations

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

Assumes

AddGroupAddGroupAddSubgroup.NormalAddSubgroup.Normal