Theorem CPolynomialAt.contDiffAt

Modification history

2024-11-25 11:42

Mathlib/Analysis/Calculus/FDeriv/Analytic.lean

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

Modified CPolynomialAt.contDiffAt View on Github →

2024-01-10 10:28

Mathlib/Analysis/Calculus/FDeriv/Analytic.lean

feat(Mathlib/Analysis/Analytic): continuously polynomial functions (#9269) …

Added CPolynomialAt.contDiffAt View on Github →