mathlib

ac0ce64c - feat(special_functions/integrals): exponential of complex multiple of x (#14623)

feat(special_functions/integrals): exponential of complex multiple of x (#14623) We add an integral for `exp (c * x)` for `c` complex (so this cannot be reduced to integration of `exp x` on the real line). This is useful for Fourier series.