Commit 2025-04-03 07:01 522230b5

View on Github →

feat: add rewriting lemmas for euclidean domains (#23076) This PR includes some equalities and equivalences about expressions in euclidean domains. They can be useful as rewriting lemmas to simplify expressions.

Estimated changes

Modified Mathlib/Algebra/EuclideanDomain/Basic.lean

added theorem EuclideanDomain.add_mul_div_left

added theorem EuclideanDomain.add_mul_div_right

added theorem EuclideanDomain.div_add_div_of_dvd

added theorem EuclideanDomain.div_div

added theorem EuclideanDomain.div_eq_div_iff_mul_eq_mul_of_dvd

added theorem EuclideanDomain.div_eq_iff_eq_mul_of_dvd

added theorem EuclideanDomain.div_mul

added theorem EuclideanDomain.div_sub_div_of_dvd

added theorem EuclideanDomain.eq_div_iff_mul_eq_of_dvd

added theorem EuclideanDomain.mul_add_div_left

added theorem EuclideanDomain.mul_add_div_right

added theorem EuclideanDomain.mul_sub_div_left

added theorem EuclideanDomain.mul_sub_div_right

added theorem EuclideanDomain.sub_mul_div_left

added theorem EuclideanDomain.sub_mul_div_right