Commit 2026-01-20 16:34 5af7f7e3

View on Github →

chore(Algebra): deprecate CancelMonoidWithZero (#33851) The ring theory library already unbundles classes like IsDomain, and it's unusual for the monoid library to use bundled cancellative classes, leading to anti-patterns synthesizing bundled from unbundled like IsDomain.toCancelMonoidWithZero. This PR removes Cancel(Comm)MonoidWithZero in favor of [(Comm)MonoidWithZero] [IsCancelMulZero]. In exchange, UniqueFactorizationMonoid and (Normalized)GCDMonoid now extend IsCancelMul. Inspired by #33832, where generalizing IsDomain.toCancelMonoidWithZero to IsCancelMulZero led to timeouts. Zulip: https://leanprover.zulipchat.com/#narrow/channel/144837-PR-reviews/topic/.2333851.20deprecate.20CancelMonoidWithZero/near/567433366 TODO: deprecate (Left/Right)CancelSemigroup/Monoid.

Estimated changes

modified theorem Finset.prod_primes_dvd
modified theorem Multiset.prod_primes_dvd
modified theorem divisor_closure_eq_closure
modified theorem Associated.eq_of_normalized
modified theorem extract_gcd
modified theorem gcd_greatest
modified theorem gcd_greatest_associated
modified theorem isUnit_gcd_of_eq_mul_gcd
modified theorem normalize_eq_normalize
modified theorem normalize_eq_normalize_iff
modified theorem Associated.of_mul_left
modified theorem Associated.of_mul_right
modified theorem DvdNotUnit.not_associated
modified theorem Prime.associated_of_dvd
modified theorem associated_of_dvd_dvd
modified theorem dvd_dvd_iff_associated
modified theorem dvd_prime_pow
modified theorem isUnit_of_associated_mul
modified theorem prime_dvd_prime_iff_eq
modified theorem prime_mul_iff
modified theorem prime_pow_iff
modified theorem eq_zero_of_mul_eq_self_left
modified theorem left_eq_mul₀
modified theorem mul_eq_left₀
modified theorem mul_eq_right₀
modified theorem mul_left_eq_self₀
modified theorem mul_right_eq_self₀
modified theorem right_eq_mul₀
added structure CancelCommMonoidWithZero
added structure CancelMonoidWithZero
modified theorem IsPrimal.mul
modified theorem dvd_and_not_dvd_iff
modified theorem mul_dvd_mul_iff_left
modified theorem mul_dvd_mul_iff_right
modified def Submonoid.isPrimal
modified theorem IsMulTorsionFree.mk'
modified theorem Polynomial.roots_normalize
modified theorem DvdNotUnit.ne
modified theorem pow_inj_of_not_isUnit
modified theorem pow_injective_of_not_isUnit
modified theorem prime_pow_succ_dvd_mul
modified theorem Prime.squarefree
modified theorem IsRadical.of_dvd
modified theorem Polynomial.primPart_ne_zero
modified theorem IsBezout.associated_gcd_gcd
modified theorem prime_factors_unique