doc(group_theory/coset): Mention "Lagrange's theorem" (#12137)

Suggested here: https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/.E2.9C.94.20Lagrange's.20Theorem.20.28Group.20theory.29/near/272469211



Co-authored-by: tb65536 <tb65536@users.noreply.github.com>

src/group_theory/coset.lean

@@ -421,7 +421,7 @@ def quotient_subgroup_of_embedding_of_le (H : subgroup α) {K L : subgroup α} (
 by rw ← fintype.card_prod;
   exact fintype.card_congr (subgroup.group_equiv_quotient_times_subgroup)
 
-/-- **Order of a Subgroup** -/
+/-- **Lagrange's Theorem**: The order of a subgroup divides the order of its ambient group. -/
 @[to_additive] lemma card_subgroup_dvd_card [fintype α] (s : subgroup α) [fintype s] :
   fintype.card s ∣ fintype.card α :=
 by classical; simp [card_eq_card_quotient_mul_card_subgroup s, @dvd_mul_left ℕ]