English
In a finite group, the order of any subgroup divides the order of the group.
Русский
Пусть группа конечна. Порядок любой ее подгруппы делит порядок всей группы.
LaTeX
$$$|s| \mid |\alpha|$$$
Lean4
/-- **Lagrange's Theorem**: The order of a subgroup divides the order of its ambient group. -/
@[to_additive /-- **Lagrange's Theorem**: The order of an additive subgroup divides the order of its
ambient additive group. -/
]
theorem card_subgroup_dvd_card (s : Subgroup α) : Nat.card s ∣ Nat.card α := by
classical simp [card_eq_card_quotient_mul_card_subgroup s, @dvd_mul_left ℕ]