Theorem has_fderiv_at_exp_smul_const

Modification history

2023-05-25 19:59
src/analysis/special_functions/exponential.lean
feat(analysis/special_functions/exponential): derivative of `u ↦ exp 𝕂 (u • x)` (#19062) …
Added has_fderiv_at_exp_smul_constView on Github →