Commit 2021-12-22 23:07 c8f0afcd
View on Github →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.