The Formal Laurent Series Field $R ((t^{- 1}))$ : Cauchy Complete, Non-Archimedean, Not Complete

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.

✓ 9 results · all verified · 6 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 3 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

1 · Prerequisites

Real Analysis

Set Theory

2 · Logical flowchart

3 · Items

Definition

The Formal Laurent Series Field $R ((t^{- 1}))$ : Cauchy Complete, Non-Archimedean, Not Complete

3 · Items

The formal Laurent series ℝ((t⁻¹)): support bounded below, valuation, leading coefficient

ℝ((t⁻¹)) is a commutative ring: the product is a finite sum and both operations preserve support bounded below

Valuation and leading coefficient in ℝ((t⁻¹)): v(fg) = v(f) + v(g), and the behaviour of v under sums

ℝ((t⁻¹)) is a field: every nonzero formal Laurent series is invertible

ℝ((t⁻¹)) is an ordered field, ordered by the sign of the leading coefficient

ℝ((t⁻¹)) is non-Archimedean, and the monomials t⁻ᵏ are cofinal below its positive elements

ℝ((t⁻¹)) does not have the least-upper-bound property; its canonical naturals have no supremum

Sequences, convergence, Cauchyness, monotonicity, boundedness and closed intervals in an arbitrary ordered field

Every Cauchy sequence in ℝ((t⁻¹)) converges: K is sequentially Cauchy complete

ℝ((t⁻¹)) has the nested interval property for lengths tending to 0

The unrestricted nested interval property fails in ℝ((t⁻¹))

The Formal Laurent Series Field R((t−1))R((t−1)): Cauchy Complete, Non-Archimedean, Not Complete

3 · Items

The formal Laurent series ℝ((t⁻¹)): support bounded below, valuation, leading coefficient

ℝ((t⁻¹)) is a commutative ring: the product is a finite sum and both operations preserve support bounded below

Valuation and leading coefficient in ℝ((t⁻¹)): v(fg) = v(f) + v(g), and the behaviour of v under sums

ℝ((t⁻¹)) is a field: every nonzero formal Laurent series is invertible

ℝ((t⁻¹)) is an ordered field, ordered by the sign of the leading coefficient

ℝ((t⁻¹)) is non-Archimedean, and the monomials t⁻ᵏ are cofinal below its positive elements

ℝ((t⁻¹)) does not have the least-upper-bound property; its canonical naturals have no supremum

Sequences, convergence, Cauchyness, monotonicity, boundedness and closed intervals in an arbitrary ordered field

Every Cauchy sequence in ℝ((t⁻¹)) converges: K is sequentially Cauchy complete

ℝ((t⁻¹)) has the nested interval property for lengths tending to 0

The unrestricted nested interval property fails in ℝ((t⁻¹))

The Formal Laurent Series Field $R ((t^{- 1}))$ : Cauchy Complete, Non-Archimedean, Not Complete