mathlib3

4dc96e4a - feat(group_theory/index): define the index of a subgroup (#8971)

feat(group_theory/index): define the index of a subgroup (#8971) Defines `subgroup.index` and proves various divisibility properties. Co-authored-by: tb65536 <tb65536@users.noreply.github.com>