Theory of univariate polynomials #
The main def is binom_expansion.
(x + y)^n can be expressed as x^n + n*x^(n-1)*y + k * y^2 for some k in the ring.
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, _⟩
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 (⇑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.
x^n - y^n can be expressed as z * (x - y) for some z in the ring.
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)}
For any polynomial f, f.eval x - f.eval y can be expressed as z * (x - y)
for some z in the ring.
Equations
- f.eval_sub_factor x y = ⟨f.sum (λ (i : ℕ) (r : R), r * (polynomial.pow_sub_pow_factor x y i).val), _⟩