mathlib3

54212007 - feat(group_theory/index): Small values of `subgroup.index` (#9893)

feat(group_theory/index): Small values of `subgroup.index` (#9893) `H.index = 1 ↔ H = ⊤` and related results. Co-authored-by: tb65536 <tb65536@users.noreply.github.com>