Taylor's estimate for the linearisation of a polynomial

By the binomial expansion f(x + h) = f(x) + f'(x) h + c h ^ 2, the derivative f'(t) at a point t linearises f near t up to an error controlled by divisibility: if d ∣ x - t, d ∣ e and e ∣ x' - x, then f(x') - f(x) - f'(t) (x' - x) is divisible by d * e. With d = π ^ (k + 1) and e = π ^ n, n ≥ k + 1, this is the estimate behind Hensel's lemma with a derivative dividing π ^ k.

Main results

• Polynomial.mul_dvd_eval_sub_eval_sub_mul: Taylor's estimate d * e ∣ f(x') - f(x) - f'(t) (x' - x).

theorem Polynomial.mul_dvd_eval_sub_eval_sub_mul {R : Type u_1} [CommRing R] (f : Polynomial R) {d e t x x' : R} (hx : d ∣ x - t) (hde : d ∣ e) (hxx' : e ∣ x' - x) : d * e ∣ eval x' f - eval x f - eval t (derivative f) * (x' - x)

Taylor's estimate. If d ∣ x - t, d ∣ e and e ∣ x' - x, then the derivative at t linearises the polynomial f from x to x' up to an error divisible by d * e.