The lowest Taylor coefficient at a root

The Taylor expansion taylor r p = p(X + r) of a polynomial p at r starts in degree p.rootMultiplicity r, and its trailing coefficient is the value at r of p divided by the largest power of X - r dividing it. This is the coefficient that survives when X - r is divided out of p as often as possible before evaluating at r; for p ≠ 0 it is nonzero (Polynomial.eval_divByMonic_pow_rootMultiplicity_ne_zero), so it is the lowest nonzero coefficient of the Taylor expansion.

Main results

• Polynomial.natTrailingDegree_taylor: the Taylor expansion at r starts in degree p.rootMultiplicity r.
• Polynomial.coeff_taylor_rootMultiplicity, Polynomial.trailingCoeff_taylor: its trailing coefficient is (p /ₘ (X - C r) ^ p.rootMultiplicity r).eval r.

theorem Polynomial.natTrailingDegree_taylor {R : Type u_1} [CommRing R] (p : Polynomial R) (r : R) : ((taylor r) p).natTrailingDegree = rootMultiplicity r p

The Taylor expansion of p at r starts in degree p.rootMultiplicity r.

theorem Polynomial.coeff_taylor_rootMultiplicity {R : Type u_1} [CommRing R] (p : Polynomial R) (r : R) : ((taylor r) p).coeff (rootMultiplicity r p) = eval r (p /ₘ (X - C r) ^ rootMultiplicity r p)

The coefficient of X ^ p.rootMultiplicity r in the Taylor expansion of p at r is the value at r of p divided by the largest power of X - r dividing it.

theorem Polynomial.trailingCoeff_taylor {R : Type u_1} [CommRing R] (p : Polynomial R) (r : R) : ((taylor r) p).trailingCoeff = eval r (p /ₘ (X - C r) ^ rootMultiplicity r p)

The trailing coefficient of the Taylor expansion of p at r is the value at r of p divided by the largest power of X - r dividing it. For p ≠ 0 this is the lowest nonzero coefficient.