Morphism_from_Integers_to_Group
Provedgroup-theoryhomomorphismintegersproofwiki
Let G be a group and g in G. The map phi: Z -> G defined by phi(n) = g^n is a group homomorphism, i.e., g^(m+n) = g^m * g^n.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Morphism_from_Integers_to_Group {G : Type _} [Group G] (g : G) : ∀ m n : ℤ, g ^ (m + n) = g ^ m * g ^ n := by sorrySource