English
The integer part of the valuation is a discrete valuation ring.
Русский
Целая часть оценки является дискретной кольцевой степенью (DVR).
LaTeX
$$$\text{IsDiscreteValuationRing}\big((v.valuation\ K).\mathrm{integer}\big)$$$
Lean4
instance : IsDiscreteValuationRing (v.valuation K).integer where
not_a_field' :=
by
simp only [ne_eq, Ideal.ext_iff, IsLocalRing.mem_maximalIdeal, mem_nonunits_iff,
Valuation.Integer.not_isUnit_iff_valuation_lt_one, Ideal.mem_bot, Subtype.forall, not_forall]
obtain ⟨π, hπ⟩ := v.valuation_exists_uniformizer K
use π
simp [Valuation.mem_integer_iff, ← WithZero.coe_one, ← ofAdd_zero, -ofAdd_neg, Subtype.ext_iff,
← (v.valuation K).map_eq_zero_iff, hπ, ← WithZero.coe_one, ← ofAdd_zero]
