Subgroup_of_Abelian_Group_is_Normal
Provedabelian-groupsnormal-subgroupsproofwiki
Every subgroup of an abelian group is normal.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Subgroup_of_Abelian_Group_is_Normal {G : Type _} [CommGroup G] (H : Subgroup G) (g h : G) (hh : h ∈ H) : g * h * g⁻¹ ∈ H := by sorrySource