mathlib

c8835190 - feat(ring_theory/unique_factorization_domain): `factors x = normalized_factors x` (#13356)

feat(ring_theory/unique_factorization_domain): `factors x = normalized_factors x` (#13356) If the group of units is trivial, an arbitrary choice of factors is exactly the unique set of normalized factors. I made this a `simp` lemma in this direction because `normalized_factors` has a stronger specification than `factors`. I believe currently we actually know less about `normalized_factors` than `factors`, so if it proves too inconvenient I can also remove the `@[simp]`.