Commit 2020-08-13 12:59 34352c2d

View on Github →

refactor(algebra/associated): change several instances from [integral_domain] to [comm_cancel_monoid_with_zero] (#3744) defines comm_cancel_monoid_with_zero replaces some integral_domain instances with comm_cancel_monoid_with_zero prepares the API for refactoring normalization_domain, gcd_domain, and unique_factorization_domain to monoids

Estimated changes

Modified src/algebra/associated.lean

modified theorem associated_mul_left_cancel

modified theorem associated_mul_right_cancel

modified theorem associates.prod_eq_zero_iff

modified theorem dvd_and_not_dvd_iff

modified theorem exists_associated_mem_of_dvd_prod

modified theorem irreducible_of_prime

modified theorem pow_dvd_pow_iff

modified theorem succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul

Modified src/algebra/divisibility.lean

added theorem mul_dvd_mul_iff_right

Modified src/algebra/group_with_zero.lean

Modified src/algebra/ring/basic.lean

deleted theorem mul_dvd_mul_iff_right