feat(Algebra/MvPolynomial/PDeriv): a coefficient formula for pderiv (#39624)

This formula is useful for defining partial derivatives of multivariate power series, see PR #39626.

Author: justus-springer

Mathlib/Algebra/MvPolynomial/PDeriv.lean

@@ -118,6 +118,21 @@ theorem pderiv_pow {i : σ} {f : MvPolynomial σ R} {n : ℕ} :
 theorem pderiv_C_mul {f : MvPolynomial σ R} {i : σ} : pderiv i (C a * f) = C a * pderiv i f := by
   rw [C_mul', Derivation.map_smul, C_mul']
 
+theorem coeff_pderiv {i : σ} (p : MvPolynomial σ R) (m : σ →₀ ℕ) :
+    coeff m (pderiv i p) = coeff (m + single i 1) p * (m i + 1) := by
+  classical
+  induction p using MvPolynomial.induction_on' with
+  | add p q hp hq => simp [hp, hq, add_mul]
+  | monomial n a =>
+    rw [pderiv_monomial, coeff_monomial, coeff_monomial]
+    by_cases h : n = m + single i 1
+    · simp [h]
+    simp only [h, ↓reduceIte, zero_mul]
+    by_cases hn : n i = 0
+    · simp [hn]
+    apply if_neg
+    rwa [tsub_eq_iff_eq_add_of_le (fun _ ↦ by grind)]
+
 theorem pderiv_map {S} [CommSemiring S] {φ : R →+* S} {f : MvPolynomial σ R} {i : σ} :
     pderiv i (map φ f) = map φ (pderiv i f) := by
   apply induction_on f (fun r ↦ by simp) (fun p q hp hq ↦ by simp [hp, hq]) fun p j eq ↦ ?_