Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-31
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.

Length and valuation in a DVR

Statement

Let V be a discrete valuation ring with uniformiser π. Then for every integer n0,

V(V/(πn))=n.

More generally, if xV is nonzero and x=uπn with u a unit, then

V(V/(x))=n.

Facts & Assumptions

Given: A discrete valuation ring V with uniformiser π.

[L1]

Every nonzero element of the fraction field of V is uniquely uπn with u a unit and nZ (Every nonzero fraction is a unit times a power of a uniformiser).

[L2]

Every nonzero ideal of V is (πn) for a unique integer n0 (Ideals in a DVR are powers of the maximal ideal).

[F1]

A composition series has finitely many simple factors, and the length is their number (Composition series and length of a module).

[L3]

Length is additive in short exact sequences (Module length is additive in short exact sequences).

Proof

technique · direct
1.1

The case n=0 is V/(1)=0, whose length is 0 by [F1]. For n=1, the ideals of V/(π) correspond to the ideals of V containing (π). By [L2], those are only (π) and V, so V/(π) is simple and has length 1.

F1L2given
2.1

For each n1 there is a short exact sequence 0(πn)/(πn+1)V/(πn+1)V/(πn)0. Multiplication by πn induces an isomorphism V/(π)(πn)/(πn+1), so step 1.1 gives V((πn)/(πn+1))=1. Therefore [L3] yields V(V/(πn+1))=V(V/(πn))+1.

L2L3step 1.1algebra
3.1

By induction on n, step 1.1 and step 2.1 give V(V/(πn))=n for every n0.

step 1.1step 2.1induction
4.1

Let xV be nonzero, and write x=uπn as in [L1]. Multiplication by the unit u1 identifies the ideals (x) and (πn), so V/(x)V/(πn) as V-modules. Hence V(V/(x))=V(V/(πn))=n.

L1step 3.1algebra

Depends on

Used by

Dependency tree · two levels

11 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