Commit 2024-11-07 11:20 8b01025f

View on Github →

chore: deprecate Nat.le_div_iff_mul_le' and Nat.div_lt_iff_lt_mul' (#18721) These duplicate the unprimed lemmas exactly (except in the names of the arguments).

Estimated changes