Theorem ContDiff.differentiable_iteratedDeriv

Modification history

2024-11-25 11:42

Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean

feat: extend `ContDiff` to take a smoothness exponent in `WithTop ℕ∞` (#19442) …

Modified ContDiff.differentiable_iteratedDeriv View on Github →

2023-06-01 10:18

Mathlib/Analysis/Calculus/IteratedDeriv.lean

feat: port Analysis.Calculus.IteratedDeriv (#4545)

Added ContDiff.differentiable_iteratedDeriv View on Github →