Theorem derivWithin_fun_const_smul_field

Modification history

2026-01-27 21:38
Mathlib/Analysis/Calculus/Deriv/Mul.lean
feat(Analysis/Calculus): generalize scalar multiplication actions (#34314) …
Added derivWithin_fun_const_smul_fieldView on Github →