Conjugate_of_Set_by_Identity
Provedconjugacyproofwiki
Conjugation by the identity leaves elements unchanged.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Conjugate_of_Set_by_Identity {G : Type _} [Group G] (s : G) : (1 : G) * s * (1 : G)⁻¹ = s := by sorrySource