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 binomial theorem over the complex field
Statement
For and , write for the canonical-natural map of The canonical natural of a field. Then The conventions and prerequisite facts used below are recorded in is a field, every element is uniquely , and every nonzero element has inverse , Integer powers in the complex field, The set of -element subsets and the binomial coefficient , Pascal's rule , and the hockey-stick identity , The product of a finite list in a monoid, by recursion, with the empty product () equal to the identity, Generalised associativity: in a monoid the product of a finite list does not depend on the bracketing, and in a commutative monoid it does not depend on the order of the factors either, The principle of mathematical induction.
Facts & Assumptions
Given: Complex and natural .
Proof
For both sides are the empty-sum convention .
Assume the formula at .
Multiply the formula in step 1.2 by , split the finite initial-segment sums, prove the shift from the recursive monoid-sum clauses, and group equal powers.
Pascal's rule gives the complex coefficient at every index, including the endpoints, so the formula holds at .
Depends on
- $\mathbb C=\mathbb R[x]/(x^2+1)$ is a field, every element is uniquely $a+bi$, and every nonzero element has inverse $(a-bi)/(a^2+b^2)$
- Integer powers in the complex field
- The set $[A]^{k}$ of $k$-element subsets and the binomial coefficient $\binom{n}{k} := \lvert [n]^{k}\rvert$
- Pascal's rule $\binom{n+1}{k+1} = \binom{n}{k} + \binom{n}{k+1}$, and the hockey-stick identity $\sum_{i \le n}\binom{i}{k} = \binom{n+1}{k+1}$
- The product $g_0 g_1 \cdots g_{n-1}$ of a finite list in a monoid, by recursion, with the empty product ($n = 0$) equal to the identity
- Generalised associativity: in a monoid the product of a finite list does not depend on the bracketing, and in a commutative monoid it does not depend on the order of the factors either
- The principle of mathematical induction
- The canonical natural $\iota(n) = n \cdot 1_F$ of a field
Used by
- Holomorphic functions are real analytic and smooth in their two real coordinates Corollary
- Characteristic functions of bernoulli binomial and poisson laws Example
- Independent sums via characteristic functions Example
- The power series of exp(z₀+z₁) on every bidisc Example
- A nonzero value of a nonconstant complex polynomial cannot be a local minimum of its modulus Lemma
- The binomial double series for re-expanding a complex power series is absolutely convergent and may be regrouped Lemma
- An absolutely convergent multi-indexed power series is holomorphic and differentiates termwise Theorem
- exp(z+w)=exp z exp w, and the complex exponential extends the real exponential Theorem
Dependency tree · two levels
41 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)