Theorem Real.abs_iteratedDeriv_cos_le_one

Modification history

2025-08-27 13:41
Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean
feat: lemmas about iterated derivatives of trig functions (#29023)
Added Real.abs_iteratedDeriv_cos_le_oneView on Github →