Theorem Irreducible.multiplicity_of_associated

Modification history

2026-10-07 11:06
Mathlib/RingTheory/Multiplicity.lean
feat(RingTheory): multiplicity at an irreducible element (#40301) …
Added Irreducible.multiplicity_of_associatedView on Github →