feat(ring_theory/unique_factorization_domain): `factors x = normalize…

…d_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]`.

src/ring_theory/unique_factorization_domain.lean

@@ -435,6 +435,18 @@ variables [unique_factorization_monoid α]
 noncomputable def normalized_factors (a : α) : multiset α :=
 multiset.map normalize $ factors a
 
+/-- An arbitrary choice of factors of `x : M` is exactly the (unique) normalized set of factors,
+if `M` has a trivial group of units. -/
+@[simp] lemma factors_eq_normalized_factors {M : Type*} [cancel_comm_monoid_with_zero M]
+  [decidable_eq M] [unique_factorization_monoid M] [unique (Mˣ)] (x : M) :
+  factors x = normalized_factors x :=
+begin
+  unfold normalized_factors,
+  convert (multiset.map_id (factors x)).symm,
+  ext p,
+  exact normalize_eq p
+end
+
 theorem normalized_factors_prod {a : α} (ane0 : a ≠ 0) : associated (normalized_factors a).prod a :=
 begin
   rw [normalized_factors, factors, dif_neg ane0],