Commit 2026-09-10 09:55 403547fe

View on Github →

refactor(RingTheory/Multiplicity): switch multiplicity to have junk value of 0 (#43573) This PR switches multiplicity to have a junk value of 0. This is more consistent with the rest of mathlib and valuations.

Estimated changes

Modified Mathlib/Algebra/Polynomial/Div.lean

Modified Mathlib/Data/Nat/Choose/Lucas.lean

Modified Mathlib/Data/Nat/Factorization/Defs.lean

modified theorem Nat.multiplicity_eq_factorization

Modified Mathlib/Data/Nat/Squarefree.lean

Modified Mathlib/FieldTheory/SeparableDegree.lean

Modified Mathlib/GroupTheory/RegularWreathProduct.lean

Modified Mathlib/NumberTheory/Padics/PadicNorm.lean

Modified Mathlib/NumberTheory/Padics/PadicVal/Basic.lean

modified theorem padicValInt.of_ne_one_ne_zero

modified theorem padicValNat_self

modified theorem padicValRat.multiplicity_sub_multiplicity

modified theorem padicValRat.of_int_multiplicity

Modified Mathlib/NumberTheory/Padics/PadicVal/Defs.lean

deleted theorem padicValNat_def'

modified theorem padicValNat_def

Modified Mathlib/RingTheory/Multiplicity.lean

modified theorem dvd_iff_emultiplicity_pos

modified theorem dvd_iff_multiplicity_pos

deleted theorem emultiplicity_eq_iff_multiplicity_eq_of_ne_one

added theorem emultiplicity_eq_iff_multiplicity_eq_of_ne_zero

modified theorem emultiplicity_eq_zero_iff_multiplicity_eq_zero

modified theorem emultiplicity_pos_iff

modified theorem emultiplicity_pos_of_dvd

deleted theorem multiplicity_eq_one_of_not_finiteMultiplicity

modified theorem multiplicity_eq_zero

added theorem multiplicity_eq_zero_of_not_dvd

added theorem multiplicity_eq_zero_of_not_finiteMultiplicity

modified theorem multiplicity_ne_zero

modified theorem multiplicity_pos_of_dvd

modified theorem multiplicity_self

modified theorem multiplicity_zero