Union_of_Conjugacy_Classes_is_Normal
Provedconjugacy-classgroup-theorynormal-subgroupproofwiki
A subgroup H of G is normal if and only if H is a union of conjugacy classes of G (equivalently, H is closed under conjugation).
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Union_of_Conjugacy_Classes_is_Normal {G : Type _} [Group G] (H : Subgroup G) : H.Normal ↔ ∀ (g : G) (h : G), h ∈ H → g * h * g⁻¹ ∈ H := by sorrySource