From 85e531ad7f4d569daa0f8464ac78e54661d85743 Mon Sep 17 00:00:00 2001 From: Justus Springer Date: Wed, 20 May 2026 17:43:17 +0100 Subject: [PATCH] coeff_pderiv --- Mathlib/Algebra/MvPolynomial/PDeriv.lean | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/Mathlib/Algebra/MvPolynomial/PDeriv.lean b/Mathlib/Algebra/MvPolynomial/PDeriv.lean index c70e5c5bb4f250..929abd0a853464 100644 --- a/Mathlib/Algebra/MvPolynomial/PDeriv.lean +++ b/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 ↦ ?_