Subgroup_is_Normal_iff_it_contains_Product_of_Inverses
Provednormal-subgroupsproofwiki
A subgroup H is normal iff for all a, b, ab ∈ H implies a⁻¹b⁻¹ ∈ H.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Subgroup_is_Normal_iff_it_contains_Product_of_Inverses {G : Type _} [Group G] (H : Subgroup G) (hN : H.Normal) (a b : G) (hab : a * b ∈ H) : a⁻¹ * b⁻¹ ∈ H := by sorrySource