Theorem UniqueFactorizationMonoid.factors_rel_of_associated

Modification history

2024-11-20 11:43
Mathlib/RingTheory/UniqueFactorizationDomain.lean
chore(RingTheory): split `UniqueFactorizationDomain.lean` (#19256) …
Modified UniqueFactorizationMonoid.factors_rel_of_associatedView on Github →
2024-10-17 19:04
Mathlib/RingTheory/UniqueFactorizationDomain.lean
feat: UniqueFactorizationMonoid.factors_rel_of_associated (#17260)
Added UniqueFactorizationMonoid.factors_rel_of_associatedView on Github →