# mathlibdocumentation

data.mv_polynomial.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 #

• mv_polynomial.pderiv i p : the partial derivative of p with respect to i.

## 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 in mv_polynomial σ R which mathematicians might call X^s

• a : R

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

• p : mv_polynomial σ R

def mv_polynomial.pderiv {R : Type u} {σ : Type u_1} (i : σ) :

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

Equations
@[simp]
theorem mv_polynomial.pderiv_monomial {R : Type u} {σ : Type u_1} {a : R} {s : σ →₀ } {i : σ} :
= (a * (s i))
@[simp]
theorem mv_polynomial.pderiv_C {R : Type u} {σ : Type u_1} {a : R} {i : σ} :
= 0
@[simp]
theorem mv_polynomial.pderiv_one {R : Type u} {σ : Type u_1} {i : σ} :
= 0
theorem mv_polynomial.pderiv_eq_zero_of_not_mem_vars {R : Type u} {σ : Type u_1} {i : σ} {f : R} (h : i f.vars) :
= 0
theorem mv_polynomial.pderiv_X {R : Type u} {σ : Type u_1} [decidable_eq σ] {i j : σ} :
= ite (i = j) 1 0
@[simp]
theorem mv_polynomial.pderiv_X_self {R : Type u} {σ : Type u_1} {i : σ} :
= 1
theorem mv_polynomial.pderiv_monomial_single {R : Type u} {σ : Type u_1} {a : R} {i : σ} {n : } :
a) = mv_polynomial.monomial (n - 1)) (a * n)
theorem mv_polynomial.pderiv_monomial_mul {R : Type u} {σ : Type u_1} {a a' : R} {s : σ →₀ } {i : σ} {s' : σ →₀ } :
a) * a') = a)) * + * a')
@[simp]
theorem mv_polynomial.pderiv_mul {R : Type u} {σ : Type u_1} {i : σ} {f g : R} :
(f * g) = f) * g + f *
@[simp]
theorem mv_polynomial.pderiv_C_mul {R : Type u} {σ : Type u_1} {a : R} {f : R} {i : σ} :
@[simp]
theorem mv_polynomial.pderiv_pow {R : Type u} {σ : Type u_1} {i : σ} {f : R} {n : } :
(f ^ n) = ((n) * f) * f ^ (n - 1)
@[simp]
theorem mv_polynomial.pderiv_nat_cast {R : Type u} {σ : Type u_1} {i : σ} {n : } :
= 0