Derivations of multivariate polynomials #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
In this file we prove that a derivation of
mv_polynomial σ R is determined by its values on all
mv_polynomial.X i. We also provide a constructor
builds a derivation from its values on
X is and a linear equivalence
σ → A and
derivation (mv_polynomial σ R) A.
The derivation on
mv_polynomial σ R that takes value
f i on