Conjugates_of_Elements_in_Centralizer
Provedcentralizerconjugationgroup-theoryproofwiki
In a group G, gag⁻¹ = hah⁻¹ if and only if g and h are in the same left coset of the centralizer of a.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Conjugates_of_Elements_in_Centralizer {G : Type _} [Group G] (a g h : G) : g * a * g⁻¹ = h * a * h⁻¹ ↔ h⁻¹ * g ∈ Subgroup.centralizer ({a} : Set G) := by sorrySource