mathlib documentation


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


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

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

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

theorem mv_polynomial.pderiv_monomial {R : Type u} {σ : Type u_1} {a : R} {s : σ →₀ } [comm_semiring R] {i : σ} :

theorem mv_polynomial.pderiv_C {R : Type u} {σ : Type u_1} {a : R} [comm_semiring R] {i : σ} :

theorem mv_polynomial.pderiv_eq_zero_of_not_mem_vars {R : Type u} {σ : Type u_1} [comm_semiring R] {i : σ} {f : mv_polynomial σ R} (h : i f.vars) :

theorem mv_polynomial.pderiv_monomial_single {R : Type u} {σ : Type u_1} {a : R} [comm_semiring R] {i : σ} {n : } :

theorem mv_polynomial.pderiv_mul {R : Type u} {σ : Type u_1} [comm_semiring R] {i : σ} {f g : mv_polynomial σ R} :

theorem mv_polynomial.pderiv_C_mul {R : Type u} {σ : Type u_1} {a : R} [comm_semiring R] {f : mv_polynomial σ R} {i : σ} :