Commit 2024-10-17 19:56 b2dddd4c

feat: sum of iterated derivatives (#16886) This introduces Polynomial.sumIDeriv, the sum of the iterated derivatives of a polynomial, to be used in particular in the proof of the Lindemann-Weierstrass theorem (see #6718). Included are:

• Polynomial.sumIDeriv_apply, Polynomial.sumIDeriv_apply_of_lt, Polynomial.sumIDeriv_apply_of_le: Polynomial.sumIDeriv expressed as a sum
• Polynomial.sumIDeriv_C, Polynomial.sumIDeriv_X: Polynomial.sumIDeriv applied to simple polynomials
• Polynomial.sumIDeriv_map: Polynomial.sumIDeriv commutes with Polynomial.map
• Polynomial.sumIDeriv_derivative: Polynomial.sumIDeriv commutes with Polynomial.derivative
• Polynomial.sumIDeriv_eq_self_add: sumIDeriv p = p + sumIDeriv (derivative p)
• Polynomial.exists_iterate_derivative_eq_factorial_smul: the k'th iterated derivative of a polynomial has a common factor k!
• Polynomial.aeval_iterate_derivative_of_lt, Polynomial.aeval_iterate_derivative_self, Polynomial.aeval_iterate_derivative_of_ge: applying Polynomial.aeval to iterated derivatives
• Polynomial.aeval_sumIDeriv, Polynomial.aeval_sumIDeriv_of_pos: applying Polynomial.aeval to Polynomial.sumIDeriv