diff --git a/Mathlib/Algebra/Polynomial/Derivative.lean b/Mathlib/Algebra/Polynomial/Derivative.lean
index af60f12660dee..63729f760cb35 100644
--- a/Mathlib/Algebra/Polynomial/Derivative.lean
+++ b/Mathlib/Algebra/Polynomial/Derivative.lean
@@ -12,6 +12,7 @@ import Mathlib.GroupTheory.GroupAction.Ring
 
 ## Main definitions
  * `Polynomial.derivative`: The formal derivative of polynomials, expressed as a linear map.
+ * `Polynomial.derivativeFinsupp`: Iterated derivatives as a finite support function.
 
 -/
 
@@ -391,6 +392,52 @@ theorem iterate_derivative_mul {n} (p q : R[X]) :
       omega
     · rw [Nat.choose_zero_right, tsub_zero]
 
+/--
+Iterated derivatives as a finite support function.
+-/
+@[simps! apply_toFun]
+noncomputable def derivativeFinsupp : R[X] →ₗ[R] ℕ →₀ R[X] where
+  toFun p := .onFinset (range (p.natDegree + 1)) (derivative^[·] p) fun i ↦ by
+    contrapose; simp_all [iterate_derivative_eq_zero, Nat.succ_le]
+  map_add' _ _ := by ext; simp
+  map_smul' _ _ := by ext; simp
+
+@[simp]
+theorem support_derivativeFinsupp_subset_range {p : R[X]} {n : ℕ} (h : p.natDegree < n) :
+    (derivativeFinsupp p).support ⊆ range n := by
+  dsimp [derivativeFinsupp]
+  exact Finsupp.support_onFinset_subset.trans (Finset.range_subset.mpr h)
+
+@[simp]
+theorem derivativeFinsupp_C (r : R) : derivativeFinsupp (C r : R[X]) = .single 0 (C r) := by
+  ext i : 1
+  match i with
+  | 0 => simp
+  | i + 1 => simp
+
+@[simp]
+theorem derivativeFinsupp_one : derivativeFinsupp (1 : R[X]) = .single 0 1 := by
+  simpa using derivativeFinsupp_C (1 : R)
+
+@[simp]
+theorem derivativeFinsupp_X : derivativeFinsupp (X : R[X]) = .single 0 X + .single 1 1 := by
+  ext i : 1
+  match i with
+  | 0 => simp
+  | 1 => simp
+  | (n + 2) => simp
+
+theorem derivativeFinsupp_map [Semiring S] (p : R[X]) (f : R →+* S) :
+    derivativeFinsupp (p.map f) = (derivativeFinsupp p).mapRange (·.map f) (by simp) := by
+  ext i : 1
+  simp
+
+theorem derivativeFinsupp_derivative (p : R[X]) :
+    derivativeFinsupp (derivative p) =
+      (derivativeFinsupp p).comapDomain Nat.succ Nat.succ_injective.injOn := by
+  ext i : 1
+  simp
+
 end Semiring
 
 section CommSemiring
diff --git a/Mathlib/Algebra/Polynomial/SumIteratedDerivative.lean b/Mathlib/Algebra/Polynomial/SumIteratedDerivative.lean
index 060e2941e11d1..9a73f63187840 100644
--- a/Mathlib/Algebra/Polynomial/SumIteratedDerivative.lean
+++ b/Mathlib/Algebra/Polynomial/SumIteratedDerivative.lean
@@ -11,6 +11,10 @@ import Mathlib.Algebra.Polynomial.RingDivision
 
 /-!
 # Sum of iterated derivatives
+
+## Main definitions
+
+* `Polynomial.sumIDeriv`: Sum of iterated derivatives of a polynomial, as a linear map
 -/
 
 open Finset
@@ -24,52 +28,6 @@ section Semiring
 
 variable [Semiring R] [Semiring S]
 
-/--
-Iterated derivatives as a finite support function.
--/
-@[simps! apply_toFun]
-noncomputable def derivativeFinsupp : R[X] →ₗ[R] ℕ →₀ R[X] where
-  toFun p := .onFinset (range (p.natDegree + 1)) (derivative^[·] p) fun i ↦ by
-    contrapose; simp_all [iterate_derivative_eq_zero, Nat.succ_le]
-  map_add' _ _ := by ext; simp
-  map_smul' _ _ := by ext; simp
-
-@[simp]
-theorem support_derivativeFinsupp_subset_range {p : R[X]} {n : ℕ} (h : p.natDegree < n) :
-    (derivativeFinsupp p).support ⊆ range n := by
-  dsimp [derivativeFinsupp]
-  exact Finsupp.support_onFinset_subset.trans (Finset.range_subset.mpr h)
-
-@[simp]
-theorem derivativeFinsupp_C (r : R) : derivativeFinsupp (C r : R[X]) = .single 0 (C r) := by
-  ext i : 1
-  match i with
-  | 0 => simp
-  | i + 1 => simp
-
-@[simp]
-theorem derivativeFinsupp_one : derivativeFinsupp (1 : R[X]) = .single 0 1 := by
-  simpa using derivativeFinsupp_C (1 : R)
-
-@[simp]
-theorem derivativeFinsupp_X : derivativeFinsupp (X : R[X]) = .single 0 X + .single 1 1 := by
-  ext i : 1
-  match i with
-  | 0 => simp
-  | 1 => simp
-  | (n + 2) => simp
-
-theorem derivativeFinsupp_map (p : R[X]) (f : R →+* S) :
-    derivativeFinsupp (p.map f) = (derivativeFinsupp p).mapRange (·.map f) (by simp) := by
-  ext i : 1
-  simp
-
-theorem derivativeFinsupp_derivative (p : R[X]) :
-    derivativeFinsupp (derivative p) =
-      (derivativeFinsupp p).comapDomain Nat.succ Nat.succ_injective.injOn := by
-  ext i : 1
-  simp
-
 /--
 Sum of iterated derivatives of a polynomial, as a linear map
 
@@ -130,9 +88,9 @@ theorem exists_iterate_derivative_eq_factorial_smul (p : R[X]) (k : ℕ) :
 
 end Semiring
 
-section CommRing
+section CommSemiring
 
-variable [CommRing R] {A : Type*} [CommRing A] [Algebra R A]
+variable [CommSemiring R] {A : Type*} [CommRing A] [Algebra R A]
 
 theorem aeval_iterate_derivative_of_lt (p : R[X]) (q : ℕ) (r : A) {p' : A[X]}
     (hp : p.map (algebraMap R A) = (X - C r) ^ q * p') {k : ℕ} (hk : k < q) :
@@ -258,6 +216,6 @@ theorem aeval_sumIDeriv' [Nontrivial A] [NoZeroDivisors A] (p : R[X]) {q : ℕ}
     rw [mem_inter, mem_Ico, mem_Ico] at hx
     exact hx.1.2.not_le hx.2.1
 
-end CommRing
+end CommSemiring
 
 end Polynomial