Commit 2024-02-22 22:14 50bf7913
View on Github →feat: Complex exp, log, and cpow are analytic (#10811)
These are all immediate from differentiability.
We also record several rewrite lemmas for switching between analyticity and differentiability. These are immediate from existing theorems, but as far as I can tell don't yet exist as iffs.