Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
doc(group_theory/index): add a theorem name and fix a to_additive (#1…
…0564) 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.
- Loading branch information