Commit 2021-12-02 03:37 34758d3f

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.