mathlib3

633c2a63 - feat(ring_theory/gauss_lemma): two primitive polynomials divide iff they do in a fraction field (#5003)

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.