Generator_of_Quotient_Groups
Provedgeneratorsgroup-theoryproofwikiquotient-group
Let N be a normal subgroup of G with N ≤ A and N ≤ B. Then the image of the join of A and B in G/N equals the join of images of A and B in G/N.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Generator_of_Quotient_Groups {G : Type _} [Group G] (N A B : Subgroup G) [hN : N.Normal] (hNA : N ≤ A) (hNB : N ≤ B) : (A ⊔ B).map (QuotientGroup.mk' N) = A.map (QuotientGroup.mk' N) ⊔ B.map (QuotientGroup.mk' N) := by sorrySource