命題
標数 p ＞ 0 の非アルキメデス的局所体(>>363)は、
有限体を係数体とする１変数形式的べき級数体(>>66)上の有限次代数である。

証明
>>431と>>459より明らかである。