Commit 2020-10-17 18:25 688157f8
View on Github →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