Theorem WfDvdMonoid.of_wellFoundedLT_associates

Modification history

2026-01-20 16:34
Mathlib/RingTheory/UniqueFactorizationDomain/Basic.lean
chore(Algebra): deprecate `CancelMonoidWithZero` (#33851) …
Modified WfDvdMonoid.of_wellFoundedLT_associatesView on Github →
2024-11-20 11:43
Mathlib/RingTheory/UniqueFactorizationDomain.lean
chore(RingTheory): split `UniqueFactorizationDomain.lean` (#19256) …
Modified WfDvdMonoid.of_wellFoundedLT_associatesView on Github →
2024-09-06 08:34
Mathlib/RingTheory/UniqueFactorizationDomain.lean
chore(RingTheory/UniqueFactorizationDomain): make `WfDvdMonoid α` an abbreviation for `IsWellFounded α DvdNotUnit` (#16145) …
Added WfDvdMonoid.of_wellFoundedLT_associatesView on Github →