Commit 2020-11-14 19:46 633c2a63

feat(ring_theory/gauss_lemma): two primitive polynomials divide iff they do in a fraction field (#5003) Shows polynomial.is_primitive.dvd_iff_fraction_map_dvd_fraction_map, that two primitive polynomials divide iff they do over a fraction field. Shows polynomial.is_primitive.int.dvd_iff_map_cast_dvd_map_cast, the version for integers and rationals.