Commit 2022-04-05 19:00 e510b204
View on Github →feat(group_theory/index): Index of intersection (#13186)
This PR adds relindex_inf_le and index_inf_le, which are companion lemmas to relindex_inf_ne_zero and index_inf_ne_zero.
feat(group_theory/index): Index of intersection (#13186)
This PR adds relindex_inf_le and index_inf_le, which are companion lemmas to relindex_inf_ne_zero and index_inf_ne_zero.