Unique_Subgroup_of_a_Given_Order_is_Normal
Provedgroup-theorynormal-subgroupproofwikiunique
If a group G has only one subgroup of a given order, then that subgroup is normal.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Unique_Subgroup_of_a_Given_Order_is_Normal {G : Type _} [Group G] (H : Subgroup G) [Fintype H] (huniq : ∀ K : Subgroup G, [Fintype K] → Fintype.card K = Fintype.card H → K = H) : H.Normal := by sorrySource