Product_of_Conjugates_equals_Conjugate_of_Products
Provedgroup-theoryproofwiki
The product of conjugates equals the conjugate of the product: (aba⁻¹)(aca⁻¹) = a(bc)a⁻¹.
Preamble
import Mathlib.Algebra.Group.Basic
Formal statement
theorem Product_of_Conjugates_equals_Conjugate_of_Products {G : Type _} [Group G] (a b c : G) : (a * b * a⁻¹) * (a * c * a⁻¹) = a * (b * c) * a⁻¹ := by sorrySource