Cyclic_Groups_of_Same_Order_are_Isomorphic
Provedcyclicgroup-theoryisomorphismproofwiki
Two cyclic groups of the same finite order are isomorphic to each other.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Cyclic_Groups_of_Same_Order_are_Isomorphic {G H : Type _} [Group G] [Group H] [IsCyclic G] [IsCyclic H] [Fintype G] [Fintype H] (h : Fintype.card G = Fintype.card H) : Nonempty (G ≃* H) := by sorrySource