mathlib

95535a3e - refactor(ring_theory/unique_factorization_domain): golf some factor_set lemmas (#9889)