Theory of univariate polynomials

The main def is Polynomial.binomExpansion.

def Polynomial.powAddExpansion {R : Type u_1} [CommSemiring R] (x : R) (y : R) (n : ℕ) : { k : R // (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.
• Polynomial.powAddExpansion x y 0 = { val := 0, property := ⋯ }
• Polynomial.powAddExpansion x y 1 = { val := 0, property := ⋯ }

def Polynomial.binomExpansion {R : Type u} [CommRing R] (f : Polynomial R) (x : R) (y : R) : { k : R // Polynomial.eval (x + y) f = Polynomial.eval x 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.

Equations

• Polynomial.binomExpansion f x y = { val := Polynomial.sum f fun (e : ℕ) (a : R) => a * ↑(Polynomial.polyBinomAux1 x y e a), property := ⋯ }

def Polynomial.powSubPowFactor {R : Type u} [CommRing R] (x : R) (y : R) (i : ℕ) : { z : R // 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.
• Polynomial.powSubPowFactor x y 0 = { val := 0, property := ⋯ }
• Polynomial.powSubPowFactor x y 1 = { val := 1, property := ⋯ }

def Polynomial.evalSubFactor {R : Type u} [CommRing R] (f : Polynomial R) (x : R) (y : R) : { z : R // Polynomial.eval x f - Polynomial.eval y f = 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

• Polynomial.evalSubFactor f x y = { val := Polynomial.sum f fun (i : ℕ) (r : R) => r * ↑(Polynomial.powSubPowFactor x y i), property := ⋯ }