Theorem Prime.finiteMultiplicity_iff_ne_zero

Modification history

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