# Documentation

Mathlib.Data.Polynomial.Identities

# Theory of univariate polynomials #

The main def is Polynomial.binomExpansion.

def Polynomial.powAddExpansion {R : Type u_1} [] (x : R) (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
• One or more equations did not get rendered due to their size.
• = { val := 0, property := (_ : (x + y) ^ 0 = x ^ 0 + 0 * x ^ (0 - 1) * y + 0 * y ^ 2) }
• = { val := 0, property := (_ : (x + y) ^ 1 = x ^ 1 + 1 * x ^ (1 - 1) * y + 0 * y ^ 2) }
Instances For
def Polynomial.binomExpansion {R : Type u} [] (f : ) (x : R) (y : R) :
{ k // Polynomial.eval (x + y) f = + Polynomial.eval x (Polynomial.derivative f) * y + 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.

Instances For
def Polynomial.powSubPowFactor {R : Type u} [] (x : R) (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
• One or more equations did not get rendered due to their size.
• = { val := 0, property := (_ : x ^ 0 - y ^ 0 = 0 * (x - y)) }
• = { val := 1, property := (_ : x ^ 1 - y ^ 1 = 1 * (x - y)) }
Instances For
def Polynomial.evalSubFactor {R : Type u} [] (f : ) (x : R) (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.

Instances For