Derivations of multivariate polynomials #
In this file we prove that a derivation of
MvPolynomial σ R is determined by its values on all
MvPolynomial.X i. We also provide a constructor
builds a derivation from its values on
X is and a linear equivalence
σ → A and
Derivation (MvPolynomial σ R) A.
If two derivations agree on
i ∈ s, then they agree on all polynomials from
MvPolynomial.supported R s.
The derivation on
MvPolynomial σ R that takes value
f i on
MvPolynomial.mkDerivation as a linear equivalence.