mathlib

688157f8 - feat(ring_theory/polynomial/content): definition of content + proof that it is multiplicative (#4393)

feat(ring_theory/polynomial/content): definition of content + proof that it is multiplicative (#4393) Defines `polynomial.content` to be the `gcd` of the coefficients of a polynomial Says a polynomial `is_primitive` if its content is 1 Proves that `(p * q).content = p.content * q.content