Theorems · Definition · group theory

QuotientAddGroup.prodEquiv

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

(G × H) / (A × B) is in bijection with G / A × H / B.

Defined in

Mathlib.GroupTheory.QuotientGroup.Basic

Cited by

3 results in Mathlib

Foundations

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

Assumes

AddGroupAddGroup