命題
F を可換環とし、A = F[[X]] を F 係数の１変数形式的べき級数環とする。
A は離散付値環(過去スレ001の645)、即ち、体でない単項イデアル整域で
局所環である。

証明
>>46より、A は整域である。
XA を X で生成される A のイデアルとする。
>>41より、A - XA の元はすべて可逆元である。
よって、XA は A の唯一の極大イデアルであり、A は局所環である。

J ≠ 0 を A の任意のイデアルとする。
n = inf { ord(f) ; f ∈ J } とする。
n = ord(f) となる f ∈ J がある。
J ≠ 0 であるから f ≠ 0 である。

f = (a_n)X^n + (a_(n+1))X^(n+1) + ...
a_n ≠ 0 とする。
f = (X^n)u
u = a_n + (a_(n+1))X + ...
と書ける。
>>41より、u は A の可逆元である。
よって、X^n ∈ J である。

g ≠ 0 を J の任意の元とする。
ord(g) ≧ n である。
上と同様に g = (X^ord(g))v と書ける。
ここで v は A の可逆元である。
よって、g は X^n で生成されるイデアル (X^n)A に含まれる。
よって、J = (X^n)A である。
よって、A は単項イデアル整域である。
証明終