Theorems · Definition · field theory

Polynomial.sumIDeriv

{R : Type u_1} → [inst : Semiring R] → Polynomial R →ₗ[R] Polynomial R

Sum of iterated derivatives of a polynomial, as a linear map This definition does not allow different weights for the derivatives. It is likely that it could be extended to allow them, but this was not needed for the initial use case (the integration by parts of the integral $I_i$ in the [Lindemann-Weierstrass](https://en.wikipedia.org/wiki/Lindemann%E2%80%93Weierstrass_theorem) theorem).

Defined in

Mathlib.Algebra.Polynomial.SumIteratedDerivative

Cited by

15 results in Mathlib

Foundations

Depth 115 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Semiring