Commit 2025-01-15 22:33 34b0940a

View on Github →

chore: typos in Fderiv instead of FDeriv (#20775)

Estimated changes

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

added theorem ContDiffWithinAt.iteratedFDerivWithin_right

deleted theorem ContDiffWithinAt.iteratedFderivWithin_right

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

Modified Mathlib/Analysis/Calculus/Rademacher.lean

added theorem LipschitzWith.hasFDerivAt_of_hasLineDerivAt_of_closure

deleted theorem LipschitzWith.hasFderivAt_of_hasLineDerivAt_of_closure

Modified Mathlib/Geometry/Manifold/MFDeriv/FDeriv.lean