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).
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).