Theorem Irreducible.finiteMultiplicity_of_not_isUnit

Modification history

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