English
For a field K with valuation v, ring O inside K, and p, define a map preVal: ModP O p → ℝ≥0 by sending 0 to 0 and x+(p) to v(algebraMap_O_K(x)) when x ≠ 0.
Русский
Для поля K с дискретной оценкой v и O ⊂ K, определим отображение preVal: ModP O p → ℝ≥0, которое отправляет 0 в 0, а x+(p) в v(алгебраическое отображение O→K)(x), если x ≠ 0.
LaTeX
$$$\mathrm{preVal}: \mathrm{ModP}(O,p) \to \mathbb{R}_{\ge 0},\quad \mathrm{preVal}(0)=0,\; \mathrm{preVal}(\overline{x})=v(\iota_O^K(x))\; (x\neq 0).$$$
Lean4
/-- For a field `K` with valuation `v : K → ℝ≥0` and ring of integers `O`,
a function `O/(p) → ℝ≥0` that sends `0` to `0` and `x + (p)` to `v(x)` as long as `x ∉ (p)`. -/
noncomputable def preVal (x : ModP O p) : ℝ≥0 :=
if x = 0 then 0 else v (algebraMap O K x.out)
