doc(group_theory/index): add a theorem name and fix a to_additive (#10564)
doc(group_theory/index): add a theorem name and fix a to_additive (#10564)

I wanted to find the theorem I know as "Lagrange's theorem" but couldn't by searching.
This PR adds the name Lagrange's theorem to the relevant file, and also fixes an extra eager `to_additive` renaming that creates a lemma `add_subgroup.index_add_card` which talks about multiplication previously.





leanprover-community/mathlib,leanprover-community/mathlib