# Partial derivatives of polynomials #

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 #

- `MvPolynomial.pderiv i p` : the partial derivative of `p` with respect to `i`, as a bundled derivation of `MvPolynomial σ R`.

## Notation #

As in other polynomial files, we typically use the notation:

- `σ : Type*` (indexing the variables)

- `R : Type*` `[CommRing R]` (the coefficients)

- `s : σ →₀ ℕ`, a function from `σ` to `ℕ` which is zero away from a finite set. This will give rise to a monomial in `MvPolynomial σ R` which mathematicians might call `X^s`

- `a : R`

- `i : σ`, with corresponding monomial `X i`, often denoted `X_i` by mathematicians

- `p : MvPolynomial σ R`

source
def MvPolynomial.pderiv {R : Type u} {σ : Type v} [CommSemiring R] (i : σ) :
Derivation R (MvPolynomial σ R) (MvPolynomial σ R)

`pderiv i p` is the partial derivative of `p` with respect to `i`

Equations

- MvPolynomial.pderiv i = MvPolynomial.mkDerivation R (Pi.single i 1)

Instances For

source
theorem MvPolynomial.pderiv_def {R : Type u} {σ : Type v} [CommSemiring R] [DecidableEq σ] (i : σ) :
pderiv i = mkDerivation R (Pi.single i 1)
source
@[simp]
theorem MvPolynomial.pderiv_monomial {R : Type u} {σ : Type v} {a : R} {s : σ →₀ ℕ} [CommSemiring R] {i : σ} :
(pderiv i) ((monomial s) a) = (monomial (s - Finsupp.single i 1)) (a * ↑(s i))
source
theorem MvPolynomial.X_mul_pderiv_monomial {R : Type u} {σ : Type v} [CommSemiring R] {i : σ} {m : σ →₀ ℕ} {r : R} :
X i * (pderiv i) ((monomial m) r) = m i • (monomial m) r
source
theorem MvPolynomial.pderiv_C {R : Type u} {σ : Type v} {a : R} [CommSemiring R] {i : σ} :
(pderiv i) (C a) = 0
source
theorem MvPolynomial.pderiv_one {R : Type u} {σ : Type v} [CommSemiring R] {i : σ} :
(pderiv i) 1 = 0
source
@[simp]
theorem MvPolynomial.pderiv_X {R : Type u} {σ : Type v} [CommSemiring R] [DecidableEq σ] (i j : σ) :
(pderiv i) (X j) = Pi.single i 1 j
source
@[simp]
theorem MvPolynomial.pderiv_X_self {R : Type u} {σ : Type v} [CommSemiring R] (i : σ) :
(pderiv i) (X i) = 1
source
@[simp]
theorem MvPolynomial.pderiv_X_of_ne {R : Type u} {σ : Type v} [CommSemiring R] {i j : σ} (h : j ≠ i) :
(pderiv i) (X j) = 0
source
theorem MvPolynomial.pderiv_eq_zero_of_notMem_vars {R : Type u} {σ : Type v} [CommSemiring R] {i : σ} {f : MvPolynomial σ R} (h : i ∉ f.vars) :
(pderiv i) f = 0
source
@[deprecated MvPolynomial.pderiv_eq_zero_of_notMem_vars (since := "2025-05-23")]
theorem MvPolynomial.pderiv_eq_zero_of_not_mem_vars {R : Type u} {σ : Type v} [CommSemiring R] {i : σ} {f : MvPolynomial σ R} (h : i ∉ f.vars) :
(pderiv i) f = 0

Alias of `MvPolynomial.pderiv_eq_zero_of_notMem_vars`.

source
theorem MvPolynomial.pderiv_monomial_single {R : Type u} {σ : Type v} {a : R} [CommSemiring R] {i : σ} {n : ℕ} :
(pderiv i) ((monomial (Finsupp.single i n)) a) = (monomial (Finsupp.single i (n - 1))) (a * ↑n)
source
theorem MvPolynomial.pderiv_mul {R : Type u} {σ : Type v} [CommSemiring R] {i : σ} {f g : MvPolynomial σ R} :
(pderiv i) (f * g) = (pderiv i) f * g + f * (pderiv i) g
source
theorem MvPolynomial.pderiv_pow {R : Type u} {σ : Type v} [CommSemiring R] {i : σ} {f : MvPolynomial σ R} {n : ℕ} :
(pderiv i) (f ^ n) = ↑n * f ^ (n - 1) * (pderiv i) f
source
theorem MvPolynomial.pderiv_C_mul {R : Type u} {σ : Type v} {a : R} [CommSemiring R] {f : MvPolynomial σ R} {i : σ} :
(pderiv i) (C a * f) = C a * (pderiv i) f
source
theorem MvPolynomial.pderiv_map {R : Type u} {σ : Type v} [CommSemiring R] {S : Type u_1} [CommSemiring S] {φ : R →+* S} {f : MvPolynomial σ R} {i : σ} :
(pderiv i) ((map φ) f) = (map φ) ((pderiv i) f)
source
theorem MvPolynomial.pderiv_rename {R : Type u} {σ : Type v} [CommSemiring R] {τ : Type u_1} {f : σ → τ} (hf : Function.Injective f) (x : σ) (p : MvPolynomial σ R) :
(pderiv (f x)) ((rename f) p) = (rename f) ((pderiv x) p)
source
theorem MvPolynomial.aeval_sumElim_pderiv_inl {R : Type u} {σ : Type v} [CommSemiring R] {S : Type u_1} {τ : Type u_2} [CommRing S] [Algebra R S] (p : MvPolynomial (σ ⊕ τ) R) (f : τ → S) (j : σ) :
(aeval (Sum.elim X (⇑C ∘ f))) ((pderiv (Sum.inl j)) p) = (pderiv j) ((aeval (Sum.elim X (⇑C ∘ f))) p)