Centralizer_in_Subgroup_is_Intersection
Provedcentralizersproofwikisubgroups
The centralizer of x in H equals the intersection of H with the centralizer of x in G.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Centralizer_in_Subgroup_is_Intersection {G : Type _} [Group G] (H : Subgroup G) (x g : G) (hg : g ∈ H) (hgx : g * x = x * g) : g ∈ H ∧ g * x = x * g := by sorrySource