Lagranges_Theorem_Group_Theory
Provedindex-of-subgroupslagrange-s-theorem-group-theoryorder-of-groupsproofwikisubgroups
Let G be a finite group and H a subgroup of G. Then |H| divides |G|.
Preamble
import Mathlib.GroupTheory.Coset.Basic import Mathlib.Tactic
Formal statement
theorem Lagranges_Theorem_Group_Theory {G : Type*} [Group G] [Fintype G] (H : Subgroup G) [Fintype H] : Fintype.card H ∣ Fintype.card G := by sorrySource