noncomputable def taylorExpansion {R : Type u_1} [CommRing R] (a : R) (f : Polynomial R) : Polynomial R

Definition 8.5 (Taylor expansion): given a polynomial $f \in R[x]$ over a commutative ring $R$ and a point $a \in R$, the Taylor expansion at $a$ is the polynomial obtained by re-expanding $f$ in powers of $X - a$. Thin wrapper around Polynomial.taylor.