mathlib documentation

data.polynomial.identities

Theory of univariate polynomials

The main def is binom_expansion.

def polynomial.pow_add_expansion {R : Type u_1} [comm_semiring R] (x y : R) (n : ℕ) :

{k // (x + y) ^ n = x ^ n + ((↑n) * x ^ (n - 1)) * y + k * y ^ 2}

Equations

polynomial.pow_add_expansion x y (n + 2) = (polynomial.pow_add_expansion x y n.succ).cases_on (λ (z : R) (hz : (x + y) ^ (n + 1) = x ^ (n + 1) + ((↑(n + 1)) * x ^ (n + 1 - 1)) * y + z * y ^ 2), ⟨x * z + (↑n + 1) * x ^ n + z * y, _⟩)
polynomial.pow_add_expansion x y 1 = ⟨0, _⟩
polynomial.pow_add_expansion x y 0 = ⟨0, _⟩

theorem polynomial.derivative_eval {R : Type u} [comm_ring R] (p : polynomial R) (x : R) :

polynomial.eval x p.derivative = finsupp.sum p (λ (n : ℕ) (a : R), (a * ↑n) * x ^ (n - 1))

def polynomial.binom_expansion {R : Type u} [comm_ring R] (f : polynomial R) (x y : R) :

{k // polynomial.eval (x + y) f = polynomial.eval x f + (polynomial.eval x f.derivative) * y + k * y ^ 2}

Equations

f.binom_expansion x y = ⟨finsupp.sum f (λ (e : ℕ) (a : R), a * (poly_binom_aux1 x y e a).val), _⟩

def polynomial.pow_sub_pow_factor {R : Type u} [comm_ring R] (x y : R) (i : ℕ) :

{z // x ^ i - y ^ i = z * (x - y)}

Equations

polynomial.pow_sub_pow_factor x y (k + 2) = (polynomial.pow_sub_pow_factor x y k.succ).cases_on (λ (z : R) (hz : x ^ (k + 1) - y ^ (k + 1) = z * (x - y)), ⟨z * x + y ^ (k + 1), _⟩)
polynomial.pow_sub_pow_factor x y 1 = ⟨1, _⟩
polynomial.pow_sub_pow_factor x y 0 = ⟨0, _⟩

def polynomial.eval_sub_factor {R : Type u} [comm_ring R] (f : polynomial R) (x y : R) :

{z // polynomial.eval x f - polynomial.eval y f = z * (x - y)}

Equations

f.eval_sub_factor x y = ⟨finsupp.sum f (λ (i : ℕ) (r : R), r * (polynomial.pow_sub_pow_factor x y i).val), _⟩