Commit 2025-04-08 08:43 eaac2230

View on Github →

feat: add rewriting lemmas for integers (#23275) This PR includes some equalities and equivalences about expressions with integer numbers. They can be useful as rewriting lemmas to simplify expressions. (See #8102 for motivation)

Estimated changes

Modified Mathlib/Data/Int/Init.lean

added theorem Int.div_le_div_iff_of_dvd_of_neg_of_neg

added theorem Int.div_le_div_iff_of_dvd_of_neg_of_pos

added theorem Int.div_le_div_iff_of_dvd_of_pos_of_neg

added theorem Int.div_le_div_iff_of_dvd_of_pos_of_pos

added theorem Int.div_le_iff_of_dvd_of_neg

added theorem Int.div_le_iff_of_dvd_of_pos

added theorem Int.div_lt_div_iff_of_dvd_of_neg_of_neg

added theorem Int.div_lt_div_iff_of_dvd_of_neg_of_pos

added theorem Int.div_lt_div_iff_of_dvd_of_pos

added theorem Int.div_lt_div_iff_of_dvd_of_pos_of_neg

added theorem Int.div_lt_iff_of_dvd_of_neg

added theorem Int.div_lt_iff_of_dvd_of_pos

added theorem Int.le_div_iff_of_dvd_of_neg

added theorem Int.le_div_iff_of_dvd_of_pos

added theorem Int.lt_div_iff_of_dvd_of_neg

added theorem Int.lt_div_iff_of_dvd_of_pos