principal_ideal_domain.to_unique_factorization_domain

The unique factorization domain structure given by the principal ideal domain.

This is not added as type class instance, since the factors might be computed in a different way. E.g. factors could return normalized values.