Theory of univariate polynomials
derivative p is the formal derivative of the polynomial p
Equations
- p.derivative = finsupp.sum p (λ (n : ℕ) (a : R), ⇑polynomial.C (a * ↑n) * polynomial.X ^ (n - 1))
theorem
polynomial.derivative_monomial
{R : Type u}
[semiring R]
(a : R)
(n : ℕ) :
(⇑polynomial.C a * polynomial.X ^ n).derivative = ⇑polynomial.C (a * ↑n) * polynomial.X ^ (n - 1)
@[simp]
theorem
polynomial.derivative_C
{R : Type u}
[semiring R]
{a : R} :
(⇑polynomial.C a).derivative = 0
@[simp]
@[simp]
theorem
polynomial.derivative_add
{R : Type u}
[semiring R]
{f g : polynomial R} :
(f + g).derivative = f.derivative + g.derivative
The formal derivative of polynomials, as additive homomorphism.
Equations
- polynomial.derivative_hom R = {to_fun := polynomial.derivative _inst_2, map_zero' := _, map_add' := _}
@[simp]
theorem
polynomial.derivative_neg
{R : Type u_1}
[ring R]
(f : polynomial R) :
(-f).derivative = -f.derivative
@[simp]
theorem
polynomial.derivative_sub
{R : Type u_1}
[ring R]
(f g : polynomial R) :
(f - g).derivative = f.derivative - g.derivative
@[simp]
theorem
polynomial.derivative_sum
{R : Type u}
{ι : Type y}
[semiring R]
{s : finset ι}
{f : ι → polynomial R} :
(s.sum (λ (b : ι), f b)).derivative = s.sum (λ (b : ι), (f b).derivative)
@[simp]
theorem
polynomial.derivative_smul
{R : Type u}
[semiring R]
(r : R)
(p : polynomial R) :
(r • p).derivative = r • p.derivative
@[simp]
theorem
polynomial.derivative_mul
{R : Type u}
[comm_semiring R]
{f g : polynomial R} :
(f * g).derivative = f.derivative * g + f * g.derivative
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) :
(polynomial.map f p).derivative = polynomial.map f p.derivative
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} :
p ≠ 0 → p.derivative.degree < p.degree
theorem
polynomial.nat_degree_derivative_lt
{R : Type u}
[comm_semiring R]
{p : polynomial R} :
p.derivative ≠ 0 → p.derivative.nat_degree < p.nat_degree
theorem
polynomial.degree_derivative_le
{R : Type u}
[comm_semiring R]
{p : polynomial R} :
p.derivative.degree ≤ p.degree
The formal derivative of polynomials, as linear homomorphism.
Equations
- polynomial.derivative_lhom R = {to_fun := polynomial.derivative ring.to_semiring, map_add' := _, map_smul' := _}
theorem
polynomial.mem_support_derivative
{R : Type u}
[integral_domain R]
[char_zero R]
(p : polynomial R)
(n : ℕ) :
@[simp]
theorem
polynomial.degree_derivative_eq
{R : Type u}
[integral_domain R]
[char_zero R]
(p : polynomial R) :
0 < p.nat_degree → p.derivative.degree = ↑(p.nat_degree - 1)