mathlib

2d17c5a2 - feat(group_theory/index): Relative index (#9780)

feat(group_theory/index): Relative index (#9780) Defines relative index between subgroups, and proves that relative index is multiplicative in towers.