Powers_of_Element_form_Subgroup
Provedcyclicgroup-theoryproofwikisubgroup
Let G be a group. For all a in G, the set {a^n : n in Z} forms a subgroup of G. In particular, a^m * a^n = a^(m+n).
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Powers_of_Element_form_Subgroup {G : Type _} [Group G] (a : G) : ∀ m n : ℤ, a ^ m * a ^ n = a ^ (m + n) := by sorrySource