Powers_of_Group_Elements
Provedgroup-theoryindex-lawspowers-abstract-algebraproofwiki
Let (G, ·) be a group with identity e. Let a ∈ G. Then the power laws hold: a^(m+n) = a^m · a^n for integers m, n.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Powers_of_Group_Elements {G : Type _} [Group G] (a : G) (m n : ℤ) : a ^ (m + n) = a ^ m * a ^ n := by sorrySource