Commit 2021-10-11 04:03 c803c8de

feat(algebra/gcd_monoid): trivial gcd on comm_group_with_zeros (#9602) This PR extends the normalization_monoid defined on comm_group_with_zeros (e.g. fields) to a normalized_gcd_monoid. This is useful if you need to take the gcd of two polynomials in a field.