Commit 2025-05-07 19:19 e0ac3e58

View on Github →

feat(Deriv): add derivWithin_comp_mul_left etc (#24601)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Calculus/Deriv/CompMul.lean

added theorem derivWithin_comp_mul_left

added theorem deriv_comp_mul_left

added theorem hasDerivWithinAt_comp_mul_left_smul_iff

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

added theorem derivWithin_const_smul'

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

modified theorem fderivWithin_const_smul_field

Modified Mathlib/Topology/Algebra/Module/LinearMap.lean

added theorem ContinuousLinearMap.one_smulRight_eq_toSpanSingleton