Formal and analytic coordinate derivatives of complex polynomials

theorem MvPolynomial.hasDerivAt_eval_updateCarlson {ι : Type u_1} (p : MvPolynomial ι ℂ) (z : ι → ℂ) (i : ι) (x : ℂ) : HasDerivAt (fun (w : ℂ) => (eval (Function.update z i w)) p) ((eval (Function.update z i x)) ((pderiv i) p)) x

Formal partial differentiation agrees with differentiating a coordinate slice. No finiteness assumption on the variable type is needed.

theorem MvPolynomial.partialDeriv_evalCarlson {ι : Type u_1} (p : MvPolynomial ι ℂ) (z : ι → ℂ) (i : ι) : CarlsonFunctions.SeveralComplexVariables.partialDerivCarlson i (fun (w : ι → ℂ) => (eval w) p) z = (eval z) ((pderiv i) p)

Coordinate differentiation of a polynomial is evaluation of its formal derivative.