Commit 2026-10-15 10:19 aa35a481

View on Github →

chore: protect various declarations related to (f)derivs (#44875) In each case, the relevant lemma shadows a definition or a lemma in the root namespace.

Estimated changes

Modified Mathlib/Analysis/Calculus/ContDiff/Comp.lean

deleted theorem ContDiff.fderiv_apply

deleted theorem ContDiffWithinAt.fderivWithin_apply

deleted theorem Continuous.fderiv

deleted theorem Continuous.fderiv_one

Modified Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean

deleted theorem HasCompactSupport.iteratedFDeriv

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

deleted theorem CPolynomialOn.fderiv

deleted theorem CPolynomialOn.iteratedFDeriv

deleted theorem HasFiniteFPowerSeriesOnBall.fderiv_eq

Modified Mathlib/Analysis/Calculus/Gradient/Basic.lean

deleted theorem HasGradientAt.fderiv_apply

deleted theorem HasGradientWithinAt.fderivWithin_apply

Modified Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean

deleted theorem ContMDiffWithinAt.mfderivWithin_const