mathlib3

08b57a55 - feat(group_theory/index): Add `index_eq_zero_of_relindex_eq_zero` (#16991)

feat(group_theory/index): Add `index_eq_zero_of_relindex_eq_zero` (#16991) This PR adds a lemma `index_eq_zero_of_relindex_eq_zero` stating that if `[K : H]` is infinite, then `[G : H]` is infinite.