Commit 2024-11-15 20:51 290eb3b9

View on Github →

refactor: make HasStrictFDerivAt a structure (#19104) This lets us hide the implementation details, and replace them with IsLittleOTVS later. We already did something similar in #8907.

Estimated changes

Modified Mathlib/Analysis/Calculus/Deriv/Inv.lean

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

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

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

added structure HasStrictFDerivAt

deleted def HasStrictFDerivAt

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

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

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

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

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

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

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

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

Modified Mathlib/Analysis/Calculus/MeanValue.lean

Modified Mathlib/MeasureTheory/Integral/FundThmCalculus.lean