Partial derivatives of polynomials #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file defines the notion of the formal partial derivative of a polynomial, the derivative with respect to a single variable. This derivative is not connected to the notion of derivative from analysis. It is based purely on the polynomial exponents and coefficients.
Main declarations #
mv_polynomial.pderiv i p
: the partial derivative ofp
with respect toi
, as a bundled derivation ofmv_polynomial σ R
.
Notation #
As in other polynomial files, we typically use the notation:
-
σ : Type*
(indexing the variables) -
R : Type*
[comm_ring R]
(the coefficients) -
s : σ →₀ ℕ
, a function fromσ
toℕ
which is zero away from a finite set. This will give rise to a monomial inmv_polynomial σ R
which mathematicians might callX^s
-
a : R
-
i : σ
, with corresponding monomialX i
, often denotedX_i
by mathematicians -
p : mv_polynomial σ R
pderiv i p
is the partial derivative of p
with respect to i
Equations
- mv_polynomial.pderiv i = let _inst : decidable_eq σ := classical.dec_eq σ in mv_polynomial.mk_derivation R (pi.single i 1)