Revision #1931 → #2516 · back to history
modifiedNatural logarithm is analytic on single-valued branchesa735f2517e3a
| Field | From #1931 | To #2516 |
|---|
| mathlib.decl | Complex.analyticAt_clog | analyticAt_clog |
| provenance | ai | ai-moderated |
modifiedSpecial functions analytic on suitable domains943e4027936e
| Field | From #1931 | To #2516 |
|---|
| mathlib.decl | analyticOnNhd_riemannZeta | analyticOn_riemannZeta |
| provenance | ai | ai-moderated |
modifiedEntire functions have infinite radius of convergence37f5ec2983b1
| Field | From #1931 | To #2516 |
|---|
| mathlib.decl | expSeries_radius_eq_top | NormedSpace.expSeries_radius_eq_top |
| provenance | ai | ai-moderated |
modifiedLogarithm continuation around the originbb06d9054dbb
| Field | From #1931 | To #2516 |
|---|
| mathlib.decl | Complex.analyticAt_clog | analyticAt_clog |
| provenance | ai | ai-moderated |