Theorems · Theorem · group theory

QuotientAddGroup.prodAddEquiv_symm_apply

∀ {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] (q : (G ⧸ A) × H ⧸ B),
  (QuotientAddGroup.prodAddEquiv A B).symm q = Quotient.liftOn₂' q.1 q.2 (fun g h => ↑(g, h)) ⋯

Defined in

Mathlib.GroupTheory.QuotientGroup.Basic

Cited by

0 results in Mathlib

Foundations

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

Assumes

AddGroupAddGroupAddSubgroup.NormalAddSubgroup.Normal