Intersection_of_Quotient_Groups
Provedgroup-theoryintersectionproofwikiquotient-group
Let N be a normal subgroup of G with N ≤ A and N ≤ B. Then the image of A ∩ B in G/N equals the intersection of images of A and B in G/N.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Intersection_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