Alphabeta MathHow statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
The complex exponential maps onto
Statement
The complex exponential maps onto . The conventions and prerequisite facts used below are recorded in Every nonzero complex number has a unique polar form with and , , , and , The natural logarithm as the inverse of the exponential function, Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm.
Facts & Assumptions
Given: .
Proof
Write with .
Put .
Cartesian exponential form and give .
Depends on
- Every nonzero complex number has a unique polar form $r(\cos\theta+i\sin\theta)$ with $r>0$ and $-\pi<\theta\le\pi$
- $\exp(x+iy)=e^x(\cos y+i\sin y)$, $|\exp(x+iy)|=e^x$, and $e^{i\pi}+1=0$
- The natural logarithm as the inverse of the exponential function
- Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm
Used by
- The exponential function omits 0 and infinity as a meromorphic map on the plane Counterexample
- Roots of a compact connected Lie group Definition
- The exponential function omits exactly zero and shows little Picard is sharp Example
- The function e^(1/z) omits zero and takes every nonzero value infinitely often near the origin Example
- A nonvanishing holomorphic function on a homologically simply connected domain has a holomorphic logarithm Theorem
- All logarithms of z≠0 are Logz+2π i k, k∈ℤ Theorem
- Equivalent characterisations of a homologically simply connected domain Theorem
- Every contour missing a point admits a continuous logarithm, unique up to a constant in 2π iℤ Theorem
- The index of a cycle about a point off its trace is an integer Theorem
Dependency tree · two levels
18 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- J. Lebl, Basic Analysis I: Complex Numbers and the Complex Exponential (standard reference, not scraped)