WittVector.discreteValuationRing

theorem WittVector.discreteValuationRing : ∀ {p : ℕ} [hp : Fact p.Prime] {k : Type u_1} [inst : Field k] [inst_1 : CharP k p] [inst_2 : PerfectRing k p], DiscreteValuationRing (WittVector p k)

This theorem states that the ring of Witt vectors over a perfect field with positive characteristic is a Discrete Valuation Ring (DVR). It applies to any natural number `p` that is prime, any type `k` that is a field, and under conditions that `k` has characteristic `p` and is a perfect ring. In other words, if we construct Witt vectors from a perfect field of positive characteristic, the resulting structure will have the properties of a Discrete Valuation Ring.

More concisely: If `k` is a perfect field of characteristic `p`, where `p` is a prime number, then the Witt vectors constructed from `k` form a Discrete Valuation Ring.