mathlib

c8f0afcd - feat(group_theory/index): Transitivity of finite relative index. (#10936)

feat(group_theory/index): Transitivity of finite relative index. (#10936) If `H` has finite relative index in `K`, and `K` has finite relative index in `L`, then `H` has finite relative index in `L`. Golfed from #9545.