theorem
formalDerivative_linear
{R : Type u_1}
[CommRing R]
(a b : R)
(f g : Polynomial R)
:
Polynomial.derivative (Polynomial.C a * f + Polynomial.C b * g) = Polynomial.C a * Polynomial.derivative f + Polynomial.C b * Polynomial.derivative g
theorem
taylor_expansion
{R : Type u_1}
[CommRing R]
(f : Polynomial R)
(a : R)
:
∃! g : Polynomial R, f = Polynomial.C (Polynomial.eval a f) + Polynomial.C (Polynomial.eval a (Polynomial.derivative f)) * (Polynomial.X - Polynomial.C a) + g * (Polynomial.X - Polynomial.C a) ^ 2