Commit 2025-05-06 13:07 8cb819ff

View on Github →

feat(Calculus): add fderivWithin_comp_smul (#24560)

Estimated changes

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

modified theorem HasFDerivWithinAt.mapsTo_tangent_cone

modified theorem HasFDerivWithinAt.uniqueDiffWithinAt

modified theorem HasFDerivWithinAt.uniqueDiffWithinAt_of_continuousLinearEquiv

added theorem fderivWithin_comp_smul

added theorem fderivWithin_comp_smul_eq_fderivWithin_smul

added theorem fderivWithin_const_smul_field

added theorem hasFDerivWithinAt_comp_smul_iff_smul

added theorem hasFDerivWithinAt_comp_smul_smul_iff