English
Let x,y be nonzero elements in ModP O p. Then the valuation-like map preVal K v O p satisfies preVal(xy) = preVal(x) preVal(y).
Русский
Пусть x,y являются ненулевыми классами в ModP O p. Тогда отображение preVal является мультипликативным: preVal(xy) = preVal(x)·preVal(y).
LaTeX
$$$\\forall x,y:\\; ModP\\ O\\ p,\\; x y \\neq 0 \\implies\\; preVal\\ K\\ v\\ O\\ p (x y) = preVal\\ K\\ v\\ O\\ p x \\cdot preVal\\ K\\ v\\ O\\ p y$$$
Lean4
theorem preVal_mul {x y : ModP O p} (hxy0 : x * y ≠ 0) : preVal K v O p (x * y) = preVal K v O p x * preVal K v O p y :=
by
have hx0 : x ≠ 0 := mt (by rintro rfl; rw [zero_mul]) hxy0
have hy0 : y ≠ 0 := mt (by rintro rfl; rw [mul_zero]) hxy0
obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective x
obtain ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective y
rw [← map_mul (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_mul, v.map_mul]
