Commit 2022-04-05 09:11 63feb1b6
View on Github →feat(group_theory/index): Add relindex_le_of_le_left and relindex_le_of_le_right (#13015)
This PR adds relindex_le_of_le_left and relindex_le_of_le_right, which are companion lemmas to relindex_eq_zero_of_le_left and relindex_eq_zero_of_le_right.