Unique factorization domains.

In a unique factorization domain each element (except zero) is uniquely represented as a multiset of irreducible factors. Uniqueness is only up to associated elements.

This is equivalent to defining a unique factorization domain as a domain in which each element (except zero) is non-uniquely represented as a multiset of prime factors. This definition is used.

To define a UFD using the traditional definition in terms of multisets of irreducible factors, use the definition of_unique_irreducible_factorization

factor_set α representation elements of unique factorization domain as multisets.

multiset α produced by factors are only unique up to associated elements, while the multisets in factor_set α are unqiue by equality and restricted to irreducible elements. This gives us a representation of each element as a unique multisets (or the added ⊤ for 0), which has a complete lattice struture. Infimum is the greatest common divisor and supremum is the least common multiple.

to_gcd_domain constructs a GCD domain out of a unique factorization domain over a normalization domain.