English
The subring of integers inside the adic completion is a discrete valuation ring.
Русский
Подкольцо целых внутри адик завершения является дискретной оценочной окружностью (DVR).
LaTeX
$$$\text{IsDiscreteValuationRing}\big(\operatorname{Subtype}\{x \mid x \in v.valuation\ K.\mathrm{integer}\} \big)$$$
Lean4
instance : IsDiscreteValuationRing (v.adicCompletionIntegers K) where
not_a_field' := by
unfold HeightOneSpectrum.adicCompletionIntegers
simp only [ne_eq, Ideal.ext_iff, Valuation.mem_maximalIdeal_iff, Ideal.mem_bot, Subtype.ext_iff,
ZeroMemClass.coe_zero, Subtype.forall, Valuation.mem_valuationSubring_iff, not_forall, exists_prop]
obtain ⟨π, hπ⟩ := v.valuation_exists_uniformizer K
use π
simp [hπ, -ofAdd_neg, ← WithZero.coe_one, ← ofAdd_zero,
← (Valued.v : Valuation (v.adicCompletion K) ℤᵐ⁰).map_eq_zero_iff]
