mathlib documentation

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 #

Notation #

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

Equations
@[simp]
theorem mv_polynomial.pderiv_monomial {R : Type u} {σ : Type u_1} {a : R} {s : σ →₀ } [comm_semiring R] {i : σ} :
@[simp]
theorem mv_polynomial.pderiv_C {R : Type u} {σ : Type u_1} {a : R} [comm_semiring R] {i : σ} :
@[simp]
theorem mv_polynomial.pderiv_one {R : Type u} {σ : Type u_1} [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_X {R : Type u} {σ : Type u_1} [comm_semiring R] {i j : σ} :
@[simp]
theorem mv_polynomial.pderiv_X_self {R : Type u} {σ : Type u_1} [comm_semiring R] {i : σ} :
theorem mv_polynomial.pderiv_monomial_single {R : Type u} {σ : Type u_1} {a : R} [comm_semiring R] {i : σ} {n : } :
@[simp]
theorem mv_polynomial.pderiv_mul {R : Type u} {σ : Type u_1} [comm_semiring R] {i : σ} {f g : mv_polynomial σ R} :
@[simp]
theorem mv_polynomial.pderiv_C_mul {R : Type u} {σ : Type u_1} {a : R} [comm_semiring R] {f : mv_polynomial σ R} {i : σ} :
@[simp]
theorem mv_polynomial.pderiv_pow {R : Type u} {σ : Type u_1} [comm_semiring R] {i : σ} {f : mv_polynomial σ R} {n : } :
(mv_polynomial.pderiv i) (f ^ n) = ((n) * (mv_polynomial.pderiv i) f) * f ^ (n - 1)
@[simp]
theorem mv_polynomial.pderiv_nat_cast {R : Type u} {σ : Type u_1} [comm_semiring R] {i : σ} {n : } :