THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
Main definitions #
Main results #
Implementation notes #
Where possible, the results in this file should be first proved in the generality of
add_monoid_algebra, and then the versions specialized to
mv_polynomial proved in terms of these.
Please ensure the declarations in this section are direct translations of
monomial 1 s, discarding terms not divisible by this.
The remainder upon division by
monomial 1 s.
Some results about dvd (