mathlib3

59ef0700 - feat(ring_theory/unique_factorization_domain): misc lemmas on factors (#14333)

feat(ring_theory/unique_factorization_domain): misc lemmas on factors (#14333) Two little lemmas on the set of factors which I needed for #12287. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>