English
There is (up to isomorphism) a natural isomorphism between the value group with zero of K and the integer-valued group ℤᵐ⁰.
Русский
Группа значений с нулём для K изоморфна (в терминах порядка) группе ℤᵐ⁰.
LaTeX
$$$$\text{ValueGroupWithZero}(K) \cong_o \mathbb{Z}^{0}.$$$$
Lean4
instance : IsDiscreteValuationRing 𝒪[K] :=
letI := IsTopologicalAddGroup.toUniformSpace K
haveI := isUniformAddGroup_of_addCommGroup (G := K)
haveI : CompactSpace (Valued.integer K) := inferInstanceAs (CompactSpace 𝒪[K])
Valued.integer.isDiscreteValuationRing_of_compactSpace
