mathlib documentation

data.polynomial.derivative

Theory of univariate polynomials

def polynomial.derivative {R : Type u} [semiring R] :

derivative p is the formal derivative of the polynomial p

Equations
theorem polynomial.coeff_derivative {R : Type u} [semiring R] (p : polynomial R) (n : ) :
p.derivative.coeff n = (p.coeff (n + 1)) * (n + 1)

@[simp]
theorem polynomial.derivative_zero {R : Type u} [semiring R] :

theorem polynomial.derivative_monomial {R : Type u} [semiring R] (a : R) (n : ) :

@[simp]
theorem polynomial.derivative_C {R : Type u} [semiring R] {a : R} :

@[simp]
theorem polynomial.derivative_X {R : Type u} [semiring R] :

@[simp]
theorem polynomial.derivative_one {R : Type u} [semiring R] :

@[simp]
theorem polynomial.derivative_add {R : Type u} [semiring R] {f g : polynomial R} :

The formal derivative of polynomials, as additive homomorphism.

Equations
@[simp]
theorem polynomial.derivative_neg {R : Type u_1} [ring R] (f : polynomial R) :

@[simp]
theorem polynomial.derivative_sub {R : Type u_1} [ring R] (f g : polynomial R) :

@[simp]
theorem polynomial.derivative_sum {R : Type u} {ι : Type y} [semiring R] {s : finset ι} {f : ι → polynomial R} :
(∑ (b : ι) in s, f b).derivative = ∑ (b : ι) in s, (f b).derivative

@[simp]
theorem polynomial.derivative_smul {R : Type u} [semiring R] (r : R) (p : polynomial R) :

@[simp]
theorem polynomial.derivative_mul {R : Type u} [comm_semiring R] {f g : polynomial R} :

theorem polynomial.derivative_pow_succ {R : Type u} [comm_semiring R] (p : polynomial R) (n : ) :
(p ^ (n + 1)).derivative = ((n + 1) * p ^ n) * p.derivative

theorem polynomial.derivative_pow {R : Type u} [comm_semiring R] (p : polynomial R) (n : ) :
(p ^ n).derivative = ((n) * p ^ (n - 1)) * p.derivative

theorem polynomial.derivative_map {R : Type u} {S : Type v} [comm_semiring R] [comm_semiring S] (p : polynomial R) (f : R →+* S) :

Chain rule for formal derivative of polynomials.

theorem polynomial.of_mem_support_derivative {R : Type u} [comm_semiring R] {p : polynomial R} {n : } :

theorem polynomial.degree_derivative_lt {R : Type u} [comm_semiring R] {p : polynomial R} :

The formal derivative of polynomials, as linear homomorphism.

Equations
@[simp]