mathlib3documentation

data.polynomial.identities

Theory of univariate polynomials #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

The main def is binom_expansion.

def polynomial.pow_add_expansion {R : Type u_1} (x y : R) (n : ) :
{k // (x + y) ^ n = x ^ n + n * x ^ (n - 1) * y + k * y ^ 2}

(x + y)^n can be expressed as x^n + n*x^(n-1)*y + k * y^2 for some k in the ring.

Equations
def polynomial.binom_expansion {R : Type u} [comm_ring R] (f : polynomial R) (x y : R) :
{k // polynomial.eval (x + y) f = + + k * y ^ 2}

A polynomial f evaluated at x + y can be expressed as the evaluation of f at x, plus y times the (polynomial) derivative of f at x, plus some element k : R times y^2.

Equations
• y = f.sum (λ (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)}

x^n - y^n can be expressed as z * (x - y) for some z in the ring.

Equations
• (k + 2) = .cases_on (λ (z : R) (hz : x ^ (k + 1) - y ^ (k + 1) = z * (x - y)), z * x + y ^ (k + 1), _⟩)
• = 1, _⟩
• = 0, _⟩
def polynomial.eval_sub_factor {R : Type u} [comm_ring R] (f : polynomial R) (x y : R) :
{z // - = z * (x - y)}

For any polynomial f, f.eval x - f.eval y can be expressed as z * (x - y) for some z in the ring.

Equations