Theorem multiplicity_zero

Modification history

2026-09-11 16:02

Mathlib/RingTheory/Multiplicity.lean

chore(RingTheory/Multiplicity): generalize API (#43716) …

Deleted multiplicity_zero View on Github →

2026-09-10 09:55

Mathlib/RingTheory/Multiplicity.lean

refactor(RingTheory/Multiplicity): switch `multiplicity` to have junk value of `0` (#43573) …

Modified multiplicity_zero View on Github →

2026-05-28 12:19

Mathlib/RingTheory/Multiplicity.lean

feat(RingTheory/Multiplicity): multiplicity x 0 = 1 (#39947)

Added multiplicity_zero View on Github →