Alphabeta MathFormal Power Series
About this page
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.
✓ 15 results · all verified · 0 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 15 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.
1 · Prerequisites
Abstract Algebra
Real Analysis
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Countability and Uncountability
- Foundations of the Real Numbers for Analysis
- Roots, Rational Powers, and Classical Inequalities
- The Formal Laurent Series Field ℝ((t⁻¹)): Cauchy Complete, Non-Archimedean, Not Complete
2 · Logical flowchart
3 · Items
Definition
Formal power series over a commutative ring and the coefficient-extraction functional [xⁿ]
Theorem
Cauchy multiplication makes R⟦ x⟧ a commutative ring containing R[x] as the finitely supported subring
Proposition
Coefficient extraction is R-linear, separates formal series, shifts under multiplication by xᵏ, and converts products to finite convolution
Definition
Order of a formal series, congruence modulo x^N, and the x-adic notions of convergence and Cauchy sequence
Lemma
Formal order is non-Archimedean under sums and additive under products over a domain
Definition
Summable families of formal series are locally finite in every coefficient range
Theorem
Summable formal families may be regrouped and rearranged, distribute over multiplication, and have well-defined locally finite products
Theorem
R⟦ x⟧ is complete in the x-adic topology and R[x] is dense by truncation
Theorem
A formal power series is a unit exactly when its constant coefficient is a unit
Corollary
For a field K, K⟦ x⟧ is a domain and its nonunits form the unique maximal ideal xK⟦ x⟧
Definition
Composition f∘ g of formal series when the outer series is a polynomial or the inner series has zero constant term
Theorem
Substitution by a zero-constant series is a ring homomorphism, and composition is associative when both inner series have zero constant coefficient
Theorem
A zero-constant formal series has a compositional inverse exactly when its linear coefficient is a unit
Definition
The formal derivative D(∑ aₙxⁿ)=∑_n≥1naₙxⁿ⁻¹
Proposition
Formal differentiation is linear and satisfies product, power, quotient, chain, and coefficient-recovery laws
Definition
Formal exponential, logarithm, and binomial powers over a commutative ℚ-algebra
Theorem
Formal exp and log are inverse homomorphisms and formal binomial powers obey the expected addition laws
Corollary
Every 1+u with u∈ xR⟦ x⟧ has a unique kth root with constant coefficient 1 in a commutative ℚ-algebra
Definition
Formal Laurent series K((x)), their order, derivative, and residue
Lemma
Formal residues satisfy integration by parts, logarithmic differentiation, and change of variables
Theorem
Lagrange–Bürmann inversion extracts coefficients of a compositional inverse and of functions of it
Theorem