card_subgroup_dvd_card — Mathlib

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 ℕ]

Похожие утверждения