Theorem Real.differentiable_iteratedDeriv_cos

Modification history

2025-08-27 13:41

Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean

feat: lemmas about iterated derivatives of trig functions (#29023)

Added Real.differentiable_iteratedDeriv_cos View on Github →