Power_of_Conjugate_equals_Conjugate_of_Power
Provedgroup-theoryproofwiki
(a * b * a⁻¹)^n = a * b^n * a⁻¹ in any group.
Preamble
import Mathlib.Algebra.Group.Basic
Formal statement
theorem Power_of_Conjugate_equals_Conjugate_of_Power {G : Type _} [Group G] (a b : G) (n : ℕ) : (a * b * a⁻¹) ^ n = a * b ^ n * a⁻¹ := by sorrySource