Theorem Real.iteratedDerivWithin_cos_Icc

Modification history

2025-08-27 21:39
Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean
feat: lemmas about iterated derivatives within real intervals (#29024) …
Added Real.iteratedDerivWithin_cos_IccView on Github →