exponential): derivative of `u ↦ exp 𝕂 (u • x)` (#19062)

Commit

2 years ago

feat(analysis/special_functions/exponential): derivative of `u ↦ exp 𝕂 (u • x)` (#19062) Revived from an old branch of @ADedecker, golfed using new lemmas that I added in the meantime.

Author

eric-wieser

Parents

5a684ce8

mathlib3 e1a18cad - feat(analysis/special_functions/exponential): derivative of `u ↦ exp 𝕂 (u • x)` (#19062)

mathlib3
e1a18cad - feat(analysis/special_functions/exponential): derivative of `u ↦ exp 𝕂 (u • x)` (#19062)