Commit 2024-12-21 09:59 adc2006c

View on Github →

feat: analytic part of Lindemann-Weierstrass (#20092)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Polynomial/SumIteratedDerivative.lean

added theorem Polynomial.aeval_sumIDeriv_eq_eval

added theorem Polynomial.eval_sumIDeriv_of_pos

modified theorem Polynomial.sumIDeriv_eq_self_add

Created Mathlib/NumberTheory/Transcendental/Lindemann/Init/AnalyticalPart.lean

added theorem LindemannWeierstrass.exp_polynomial_approx

added theorem LindemannWeierstrass.hasDerivAt_cexp_mul_sumIDeriv

added theorem LindemannWeierstrass.integral_exp_mul_eval