How 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.
Integer powers in the complex field
Definition
Fix . Apply The recursion theorem to the set , the initial value , and the function . This defines the natural powers uniquely by
Let be the embedding of The naturals embed in the integers. For an integer , that lemma gives a unique with ; define . If and , there is a unique with and ; define The inverse exists because is a field by is a field, every element is uniquely , and every nonzero element has inverse . Thus nonnegative integer powers are defined for every , while negative integer powers are defined exactly when ; in particular and no negative power of is defined. The integer and its unique natural representative are never conflated.
Depends on
Used by
- A nonvanishing holomorphic function on such a domain has holomorphic roots of every positive order Corollary
- Complex de Moivre formula for every integer exponent Corollary
- For n≥2, the sum of all n-th roots of unity is zero Corollary
- The coefficients of a complex power series are its derivatives at the centre divided by the corresponding factorials Corollary
- The higher-derivative form of the global Cauchy formula Corollary
- The disc algebra is unital and separating but not self-adjoint or dense Counterexample
- Complex series, absolute convergence, complex power series, and radius of convergence Definition
- Formal complex polynomials, evaluation, degree, leading coefficient, and monic polynomials Definition
- Multi-indexed power series in ℂᵐ and their absolute convergence Definition
- The complex exponential by its power series Definition
- The power series of z₀/(1-z₁) and the shape of its domain of convergence Example
- Trigonometric polynomials are uniformly dense on the unit circle Example
- Cauchy-kernel contour integrals may be differentiated by a direct difference-quotient estimate Lemma
- The binomial theorem over the complex field Lemma
- The Cauchy kernel expands as an absolutely and uniformly convergent multi-indexed geometric series Lemma
- The Cauchy transform of a cycle is holomorphic off its trace, with the expected derivatives Lemma
- A continuous separately holomorphic function is the sum of an absolutely convergent power series with Cauchy-integral coefficients on every smaller polydisc Theorem
- An absolutely convergent multi-indexed power series is holomorphic and differentiates termwise Theorem
- Branch-defined complex powers agree with integer powers Theorem
- Cauchy estimates for mixed derivatives on a polydisc Theorem
- Euler's formula: exp(iθ)=cosθ+i sinθ for every real θ Theorem
- On a positively oriented circle about a, the integral of (z-a)ᵐ is zero for every integer m except -1, and is 2 pi i for m=-1 Theorem
- The n-th roots of a complex number and the n distinct roots of unity for every n≥1 Theorem
Dependency tree · two levels
19 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)