English
For x ∈ O with hx ≠ 0 in the quotient, preVal of the representative equals v(algebraMap_O_K(x)).
Русский
Для x ∈ O с ненулевым представителем в фактор-модуле, preVal представителя равен v(algebraMap_O_K(x)).
LaTeX
$$$\text{preVal}_{K,v,O,p}(\mathrm{Ideal.Quotient.mk}\_{O}(x)) = v(\iota_O^K(x))$$$
Lean4
theorem preVal_mk {x : O} (hx : (Ideal.Quotient.mk _ x : ModP O p) ≠ 0) :
preVal K v O p (Ideal.Quotient.mk _ x) = v (algebraMap O K x) :=
by
obtain ⟨r, hr⟩ : ∃ (a : O), a * (p : O) = (Ideal.Quotient.mk _ x).out - x :=
Ideal.mem_span_singleton'.1 <| Ideal.Quotient.eq.1 <| Quotient.sound' <| Quotient.mk_out' _
refine (if_neg hx).trans (v.map_eq_of_sub_lt <| lt_of_not_ge ?_)
rw [← RingHom.map_sub, ← hr, hv.le_iff_dvd]
exact fun hprx => hx (Ideal.Quotient.eq_zero_iff_mem.2 <| Ideal.mem_span_singleton.2 <| dvd_of_mul_left_dvd hprx)
