In this file we prove that a derivation of mv_polynomial σ R is determined by its values on all
monomials mv_polynomial.X i. We also provide a constructor mv_polynomial.mk_derivation that
builds a derivation from its values on X is and a linear equivalence
mv_polynomial.equiv_derivation between σ → A and derivation (mv_polynomial σ R) A.
mv_polynomial σ R
σ → A
derivation (mv_polynomial σ R) A
The derivation on mv_polynomial σ R that takes value f i on X i, as a linear map.
Use mv_polynomial.mk_derivation instead.
If two derivations agree on X i, i ∈ s, then they agree on all polynomials from
mv_polynomial.supported R s.
i ∈ s
mv_polynomial.supported R s
The derivation on mv_polynomial σ R that takes value f i on X i.
mv_polynomial.mk_derivation as a linear equivalence.