feat(ring_theory/polynomial/content): monic polynomials are primitive (#4862)
feat(ring_theory/polynomial/content): monic polynomials are primitive (#4862)

Adds the lemma `monic.is_primitive`.





leanprover-community/mathlib,leanprover-community/mathlib