Subgroup_of_Finite_Cyclic_Group_is_Determined_by_Order
Provedcyclicgroup-theoryproofwikisubgroup
In a finite cyclic group, subgroups of the same order are equal. That is, there exists exactly one subgroup of each order dividing n.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Subgroup_of_Finite_Cyclic_Group_is_Determined_by_Order {G : Type _} [Group G] [Fintype G] [IsCyclic G] [DecidableEq G] (H K : Subgroup G) [Fintype H] [Fintype K] (heq : Fintype.card H = Fintype.card K) : H = K := by sorrySource