Commit 2026-09-11 16:02 cda5e41e

View on Github →

chore(RingTheory/Multiplicity): generalize API (#43716) This PR generalizes a few basic API lemmas in RingTheory/Multiplicity.lean and also adds the missing multiplicity_one_left.

Estimated changes

Modified Mathlib/NumberTheory/Multiplicity.lean

Modified Mathlib/NumberTheory/RamificationInertia/Ramification.lean

Modified Mathlib/NumberTheory/Real/Irrational.lean

Modified Mathlib/RingTheory/DedekindDomain/Factorization.lean

Modified Mathlib/RingTheory/Multiplicity.lean

deleted theorem FiniteMultiplicity.one_right

deleted theorem emultiplicity_zero

added theorem emultiplicity_zero_right

modified theorem multiplicity_of_isUnit_right

deleted theorem multiplicity_of_one_right

modified theorem multiplicity_of_unit_right

added theorem multiplicity_one_left

added theorem multiplicity_one_right

deleted theorem multiplicity_zero

deleted theorem multiplicity_zero_eq_zero_of_ne_zero

added theorem multiplicity_zero_left

added theorem multiplicity_zero_right

Modified Mathlib/RingTheory/Valuation/PrimeMultiplicity.lean