Commit 2026-02-05 00:24 0a7aabb2

View on Github →

chore(FDeriv/Const): generalize to a TVS (#34833) Proofs about fderiv/fderivWithin were changed to avoid extra typeclass assumptions. Also replace one simp only with simp, since the default simp set works here.

Estimated changes

Modified Mathlib/Analysis/Calculus/FDeriv/Const.lean

modified theorem fderiv_const_apply

modified theorem fderiv_of_notMem_tsupport