Theorem Continuous.fderiv_one

Modification history

2026-10-15 10:19
Mathlib/Analysis/Calculus/ContDiff/Comp.lean
chore: protect various declarations related to (f)derivs (#44875) …
Deleted Continuous.fderiv_oneView on Github →
2026-02-03 17:15
Mathlib/Analysis/Calculus/ContDiff/Basic.lean
refactor(Analysis/Calculus): split long file `ContDiff/Basic.lean` (#34764) …
Modified Continuous.fderiv_oneView on Github →
2025-05-13 11:52
Mathlib/Analysis/Calculus/ContDiff/Basic.lean
feat: fun_prop for ContDiff (#24056) …
Added Continuous.fderiv_oneView on Github →