Theorem Differentiable.apply_le_of_iteratedDeriv_alternating

Modification history

2024-10-20 13:19
Mathlib/Analysis/Complex/Positivity.lean
feat(Analysis/Complex/Positivity): new file (#17862) …
Added Differentiable.apply_le_of_iteratedDeriv_alternatingView on Github →