Order_of_Homomorphic_Image_of_Group_Element
Provedgroup-theoryhomomorphismorderproofwiki
Let phi: G -> H be a group homomorphism and g in G have finite order. Then the order of phi(g) divides the order of g.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Order_of_Homomorphic_Image_of_Group_Element {G H : Type _} [Group G] [Group H] (phi : G →* H) (g : G) : orderOf (phi g) ∣ orderOf g := by sorrySource