Mathlib v3 is deprecated. Go to Mathlib v4

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_ballView on Github →