Theorem fderiv_const_smul_field

Modification history

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