Powers_of_Commutative_Elements_in_Groups
Provedcommutativitygroup-theoryproofwiki
In a group, if a and b commute, then (a * b)^n = a^n * b^n for all integers n.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Powers_of_Commutative_Elements_in_Groups {G : Type _} [Group G] (a b : G) (hab : a * b = b * a) (n : ℤ) : (a * b) ^ n = a ^ n * b ^ n := by sorrySource