mathlib3

6f3d9053 - refactor(ring_theory/polynomial/content): Define is_primitive more generally (#7316)

refactor(ring_theory/polynomial/content): Define is_primitive more generally (#7316) The lemma `is_primitive_iff_is_unit_of_C_dvd` shows that `polynomial.is_primitive` can be defined without the `gcd_monoid` assumption.