Powers_of_Commutative_Elements_in_Semigroups
Provedcommutativityproofwikisemigroup
In a semigroup, 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_Semigroups {S : Type _} [Monoid S] (a b : S) (hab : a * b = b * a) (n : ℕ) : (a * b) ^ n = a ^ n * b ^ n := by sorrySource