Powers_of_Commutative_Elements_in_Monoids
Provedcommutativitymonoidproofwiki
In a monoid, if a and b commute, then (a * b)^n = a^n * b^n for all natural numbers n.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Powers_of_Commutative_Elements_in_Monoids {M : Type _} [Monoid M] (a b : M) (hab : a * b = b * a) (n : ℕ) : (a * b) ^ n = a ^ n * b ^ n := by sorrySource