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
def polynomial.binom_expansion {R : Type u} [comm_ring R] (f : polynomial R) (x y : R) :

Equations
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
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