mathlib3

5a790471 - feat(group_theory/index): `relindex_eq_zero_of_le_left` (#10902)

feat(group_theory/index): `relindex_eq_zero_of_le_left` (#10902) If `K` has infinite index in `L`, then so does any `H ≤ K`. The `right`-version is forthcoming. Making the subgroups explicit in `relindex_mul_relindex` makes rewriting much easier (both in this situation, and in others).