mathlib3

49d2191b - feat(data/polynomial/basic): monomial_neg (#6422)

feat(data/polynomial/basic): monomial_neg (#6422) The monomial of a negation is the negation of the monomial. (this PR is part of the irreducibility saga)