Commit 2026-01-27 21:38 9754d542

View on Github →

feat(Analysis/Calculus): generalize scalar multiplication actions (#34314) Relax hypotheses on smul lemmas about deriv and fderiv. Also unify fderivWithin_const_smul_field and fderivWithin_const_smul_of_field which are duplicates.

<!-- Your PR title will become the first line of the commit message. In this box, the text above the `

Estimated changes

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

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

deleted theorem derivWithin_const_smul'

added theorem derivWithin_const_smul_field

modified theorem derivWithin_div_const

deleted theorem derivWithin_fun_const_smul'

added theorem derivWithin_fun_const_smul_field

deleted theorem deriv_const_smul'

added theorem deriv_const_smul_field

deleted theorem deriv_fun_const_smul'

added theorem deriv_fun_const_smul_field

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

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

added theorem fderivWithin_const_smul_field

deleted theorem fderivWithin_const_smul_of_field

added theorem fderiv_const_smul_field

deleted theorem fderiv_const_smul_of_field

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

deleted theorem fderivWithin_const_smul_field

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

Modified Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean