Centralizer_of_Group_Element_is_Subgroup

import Mathlib.Analysis.Complex.Basic

theorem Centralizer_of_Group_Element_is_Subgroup {G : Type _} [Group G] (a x y : G) (hx : x * a = a * x) (hy : y * a = a * y) : (x * y) * a = a * (x * y) := by sorry