Documentation

Mathlib.Algebra.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 #

Notation #

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

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

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

Equations
Instances For
    @[simp]
    theorem MvPolynomial.pderiv_monomial {R : Type u} {σ : Type v} {a : R} {s : σ →₀ } [CommSemiring R] {i : σ} :
    theorem MvPolynomial.pderiv_C {R : Type u} {σ : Type v} {a : R} [CommSemiring R] {i : σ} :
    (MvPolynomial.pderiv i) (MvPolynomial.C a) = 0
    theorem MvPolynomial.pderiv_one {R : Type u} {σ : Type v} [CommSemiring R] {i : σ} :
    @[simp]
    theorem MvPolynomial.pderiv_X {R : Type u} {σ : Type v} [CommSemiring R] [DecidableEq σ] (i : σ) (j : σ) :
    @[simp]
    theorem MvPolynomial.pderiv_X_self {R : Type u} {σ : Type v} [CommSemiring R] (i : σ) :
    @[simp]
    theorem MvPolynomial.pderiv_X_of_ne {R : Type u} {σ : Type v} [CommSemiring R] {i : σ} {j : σ} (h : j i) :
    theorem MvPolynomial.pderiv_eq_zero_of_not_mem_vars {R : Type u} {σ : Type v} [CommSemiring R] {i : σ} {f : MvPolynomial σ R} (h : if.vars) :
    theorem MvPolynomial.pderiv_mul {R : Type u} {σ : Type v} [CommSemiring R] {i : σ} {f : MvPolynomial σ R} {g : MvPolynomial σ R} :
    theorem MvPolynomial.pderiv_pow {R : Type u} {σ : Type v} [CommSemiring R] {i : σ} {f : MvPolynomial σ R} {n : } :
    (MvPolynomial.pderiv i) (f ^ n) = n * f ^ (n - 1) * (MvPolynomial.pderiv i) f
    theorem MvPolynomial.pderiv_C_mul {R : Type u} {σ : Type v} {a : R} [CommSemiring R] {f : MvPolynomial σ R} {i : σ} :
    (MvPolynomial.pderiv i) (MvPolynomial.C a * f) = MvPolynomial.C a * (MvPolynomial.pderiv i) f
    theorem MvPolynomial.pderiv_map {R : Type u} {σ : Type v} [CommSemiring R] {S : Type u_1} [CommSemiring S] {φ : R →+* S} {f : MvPolynomial σ R} {i : σ} :