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.





leanprover-community/mathlib,leanprover-community/mathlib