Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-10 23:48 0b87b0ae

View on Github →

chore(algebra/group_with_zero/defs: Rename comm_cancel_monoid_with_zero to cancel_comm_monoid_with_zero (#10669) We currently have cancel_comm_monoid but comm_cancel_monoid_with_zero. This renames the latter to follow the former. Replaced comm_cancel_ by cancel_comm_ everywhere.

Estimated changes

modified theorem associated.of_mul_left
modified theorem associated.of_mul_right
modified theorem dvd_and_not_dvd_iff
modified theorem pow_dvd_pow_iff
modified theorem prime.associated_of_dvd
modified theorem mul_dvd_mul_iff_right
modified theorem prime.squarefree
modified def associates.{u}
modified theorem prime_factors_irreducible
modified theorem prime_factors_unique
modified theorem ufm_of_gcd_of_wf_dvd_monoid