Commit 2026-10-07 11:06 27915224

View on Github →

feat(RingTheory): multiplicity at an irreducible element (#40301) Computes multiplicity p q at an irreducible q, for an arbitrary p, with Irreducible.multiplicity_self as a special case. Also, proves that a non-unit has finite multiplicity at an irreducible element. In a UniqueFactorizationMonoid, proves that two nonzero elements are associated iff they have the same multiplicity at every prime. :robot: This PR was extracted from the SKW project by Claude.

Estimated changes

Modified Mathlib/Algebra/Prime/Defs.lean

added theorem Irreducible.isUnit_of_mul_self_dvd

Modified Mathlib/Algebra/Squarefree/Basic.lean

modified theorem Irreducible.squarefree

Modified Mathlib/RingTheory/Multiplicity.lean

added theorem Irreducible.finiteMultiplicity_of_not_isUnit

added theorem Irreducible.multiplicity_eq_ite

added theorem Irreducible.multiplicity_of_associated

added theorem multiplicity_of_isUnit_left

Modified Mathlib/RingTheory/UniqueFactorizationDomain/Multiplicity.lean

added theorem Prime.finiteMultiplicity_iff_ne_zero

added theorem UniqueFactorizationMonoid.associated_iff_multiplicity_eq

added theorem UniqueFactorizationMonoid.dvd_iff_multiplicity_le