mathlib3

c7d6a8e7 - feat(ring_theory/unique_factorization_domain): descending chain condition for divisibility (#4031)

feat(ring_theory/unique_factorization_domain): descending chain condition for divisibility (#4031) Defines the strict divisibility relation `dvd_not_unit` Defines class `wf_dvd_monoid`, indicating that `dvd_not_unit` is well-founded Provides instances of `wf_dvd_monoid` Prepares to refactor `unique_factorization_domain` as a predicate extending `wf_dvd_monoid` Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com> Co-authored-by: Vierkantor <vierkantor@vierkantor.com>