Order_of_Isomorphic_Image_of_Group_Element
Provedgroup-theoryisomorphismorderproofwiki
Let phi: G -> H be a group isomorphism. Then for any a in G, orderOf(phi(a)) = orderOf(a).
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Order_of_Isomorphic_Image_of_Group_Element {G H : Type _} [Group G] [Group H] (phi : G ≃* H) (a : G) : orderOf (phi a) = orderOf a := by sorrySource