Theorem Irreducible.multiplicity_eq_ite

Modification history

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