mathlib

ef5c1d50 - feat(analysis/special_functions/pow): smoothness of `complex.cpow` (#6447)

feat(analysis/special_functions/pow): smoothness of `complex.cpow` (#6447) * `x ^ y` is smooth in both variables at `(x, y)`, if `0 < re x` or `im x ≠ 0`; * `x ^ y` is smooth in `y` if `x ≠ 0` or `y ≠ 0`.