Theorem UniqueFactorizationMonoid.dvd_iff_multiplicity_le

Modification history

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