Commit 2025-03-29 13:22 35ae6826

View on Github →

feat: lemmas about division of natural numbers (#23100) This PR includes some equalities and equivalences about expressions with natural numbers. They can be useful as rewriting lemmas to simplify expressions.

Estimated changes

Modified Mathlib/Data/Nat/Init.lean

added theorem Nat.div_le_iff_le_mul_of_dvd

added theorem Nat.eq_div_iff_mul_eq_left

added theorem Nat.lt_div_iff_mul_lt_of_dvd

added theorem Nat.mul_add_mul_div_of_dvd

added theorem Nat.mul_sub_div_of_dvd

added theorem Nat.mul_sub_mul_div_of_dvd

added theorem Nat.sub_mul_div'