mathlib3

777f11c8 - feat(group_theory/index): Special cases of relindex (#9831)

feat(group_theory/index): Special cases of relindex (#9831) Adds special cases of relindex. Also refactors the file to use `nat.card`, rather than the equivalent `(# _).to_nat`. Co-authored-by: tb65536 <tb65536@users.noreply.github.com>