Inverse_of_Inner_Automorphism
Provedautomorphismgroup-theoryinner-automorphismproofwiki
For a group G and x in G, the inverse of the inner automorphism κ_x is κ_{x⁻¹}.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Inverse_of_Inner_Automorphism {G : Type _} [Group G] (x : G) : (MulAut.conj x)⁻¹ = MulAut.conj x⁻¹ := by sorrySource