Homomorphism_of_Power_of_Group_Element
Provedgroup-theoryhomomorphismproofwiki
Let G and H be groups and phi: G -> H be a group homomorphism. Then for all integers n and elements g in G, phi(g^n) = phi(g)^n.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Homomorphism_of_Power_of_Group_Element {G H : Type _} [Group G] [Group H] (phi : G →* H) (g : G) (n : ℤ) : phi (g ^ n) = (phi g) ^ n := by sorrySource