Intersection_of_Normal_Subgroups_is_Normal
Provedgroup-theoryintersectionnormal-subgroupproofwiki
The intersection (infimum) of any family of normal subgroups of a group is normal.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Intersection_of_Normal_Subgroups_is_Normal {G : Type _} [Group G] {I : Type _} (N : I → Subgroup G) (hN : ∀ i, (N i).Normal) : (⨅ i, N i).Normal := by sorrySource