Theorem Real.iteratedDerivWithin_cosh_Icc

Modification history

2025-12-09 06:39
Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean
refactor: split long file Analysis.SpecialFunctions.Trigonometric.Deriv (#32605) …
Modified Real.iteratedDerivWithin_cosh_IccView on Github →
2025-08-27 21:39
Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean
feat: lemmas about iterated derivatives within real intervals (#29024) …
Added Real.iteratedDerivWithin_cosh_IccView on Github →