Commit 2021-04-23 07:17 6f3d9053
View on Github →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.