English
DerivativeFinsupp is the structure mapping a polynomial p to the finitely supported function i ↦ derivative^[i] p, i.e., the i-th iterate of the derivative at each index.
Русский
DerivativeFinsupp — это отображение, которое полином p за вершину отображает в конечное множество индексов i ↦ derivative^i p, то есть i-я производная p.
LaTeX
$$$$ \text{derivativeFinsupp}(p) \in \mathbb{N} \to_0 R[X], \quad (\text{derivativeFinsupp}(p))(i) = (\operatorname{derivative})^{i} p $$$$
Lean4
/-- 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
