Theorem has_fderiv_at_exp_smul_const_of_mem_ball'

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_const_of_mem_ball'View on Github →