# Documentation

Mathlib.Data.MvPolynomial.PDeriv

# 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

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

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

Instances For
theorem MvPolynomial.pderiv_def {R : Type u} {σ : Type v} [] [] (i : σ) :
@[simp]
theorem MvPolynomial.pderiv_monomial {R : Type u} {σ : Type v} {a : R} {s : σ →₀ } [] {i : σ} :
↑() (↑() a) = ↑(MvPolynomial.monomial (s - fun₀ | i => 1)) (a * ↑(s i))
theorem MvPolynomial.pderiv_C {R : Type u} {σ : Type v} {a : R} [] {i : σ} :
↑() (MvPolynomial.C a) = 0
theorem MvPolynomial.pderiv_one {R : Type u} {σ : Type v} [] {i : σ} :
↑() 1 = 0
@[simp]
theorem MvPolynomial.pderiv_X {R : Type u} {σ : Type v} [] [] (i : σ) (j : σ) :
↑() () = Pi.single i 1 j
@[simp]
theorem MvPolynomial.pderiv_X_self {R : Type u} {σ : Type v} [] (i : σ) :
↑() () = 1
@[simp]
theorem MvPolynomial.pderiv_X_of_ne {R : Type u} {σ : Type v} [] {i : σ} {j : σ} (h : j i) :
↑() () = 0
theorem MvPolynomial.pderiv_eq_zero_of_not_mem_vars {R : Type u} {σ : Type v} [] {i : σ} {f : } (h : ¬) :
↑() f = 0
theorem MvPolynomial.pderiv_monomial_single {R : Type u} {σ : Type v} {a : R} [] {i : σ} {n : } :
↑() (↑(MvPolynomial.monomial fun₀ | i => n) a) = ↑(MvPolynomial.monomial fun₀ | i => n - 1) (a * n)
theorem MvPolynomial.pderiv_mul {R : Type u} {σ : Type v} [] {i : σ} {f : } {g : } :
↑() (f * g) = ↑() f * g + f * ↑() g
theorem MvPolynomial.pderiv_C_mul {R : Type u} {σ : Type v} {a : R} [] {f : } {i : σ} :
↑() (MvPolynomial.C a * f) = MvPolynomial.C a * ↑() f