Commit 2021-10-23 08:22 2cbd4bad

feat(group_theory/index): relindex_dvd_of_le_left (#9835) If H ≤ K, then K.relindex L ∣ H.relindex L. Caution: relindex_dvd_of_le_right is not true. relindex_le_of_le_right is true, but it is harder to prove, and harder to state (because you have to be careful about relindex = 0).