Commit 2024-09-06 08:34 754844d6
View on Github →chore(RingTheory/UniqueFactorizationDomain): make WfDvdMonoid α an abbreviation for IsWellFounded α DvdNotUnit (#16145)
We also rewrite some WellFounded ((· < ·) : α → α → Prop) lemmas in terms of the much less clunky WellFoundedLT α.