mathlib3

2ae199f1 - refactor(ring_theory/unique_factorization_domain): completes the refactor of `unique_factorization_domain` (#4156)

refactor(ring_theory/unique_factorization_domain): completes the refactor of `unique_factorization_domain` (#4156) Refactors `unique_factorization_domain` to `unique_factorization_monoid` `unique_factorization_monoid` is a predicate `unique_factorization_monoid` now requires no additive/subtractive structure Co-authored-by: Aaron Anderson <65780815+awainverse@users.noreply.github.com>