Theorem UniqueFactorizationMonoid.associated_iff_multiplicity_eq

Modification history

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