English
For x,y ∈ ModP O p, preVal(x+y) ≤ max(preVal(x), preVal(y)).
Русский
Для x,y ∈ ModP O p выполняется preVal(x+y) ≤ max(preVal(x), preVal(y)).
LaTeX
$$$\mathrm{preVal}(x+y) \le \max\{\mathrm{preVal}(x), \mathrm{preVal}(y)\}$$$
Lean4
theorem preVal_add (x y : ModP O p) : preVal K v O p (x + y) ≤ max (preVal K v O p x) (preVal K v O p y) :=
by
by_cases hx0 : x = 0
· rw [hx0, zero_add]; exact le_max_right _ _
by_cases hy0 : y = 0
· rw [hy0, add_zero]; exact le_max_left _ _
by_cases hxy0 : x + y = 0
· rw [hxy0, preVal_zero]; exact zero_le _
obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective x
obtain ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective y
rw [← map_add (Ideal.Quotient.mk (Ideal.span {↑p})) r s] at hxy0 ⊢
rw [preVal_mk hv hx0, preVal_mk hv hy0, preVal_mk hv hxy0, RingHom.map_add]; exact v.map_add _ _
