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.





leanprover-community/mathlib,leanprover-community/mathlib