English
Let the integer part of the valuation associated to a height-one prime in a Dedekind domain be a principal ideal ring.
Русский
Пусть целочисленная часть соответствующей едва ли нормализованной оценки при высоте единицы в раскладе Дедекдинова домена образует кольцо главных идеалов.
LaTeX
$$$\text{IsPrincipalIdealRing}\big((v.valuation\ K).\mathrm{integer}\big)$$$
Lean4
instance : IsPrincipalIdealRing (v.valuation K).integer :=
by
rw [(Valuation.integer.integers (v.valuation K)).isPrincipalIdealRing_iff_not_denselyOrdered,
WithZero.denselyOrdered_set_iff_subsingleton]
simpa using (v.valuation K).toMonoidWithZeroHom.range_nontrivial
