English
For any f in PreTilt(O, p), val(K, v, O, hv, p)(f) = 0 if and only if f = 0. The valuation detects zero elements.
Русский
Для любого f в PreTilt(O, p) значение валюции равно нулю тогда и только тогда, когда f = 0. Валюация распознаёт нулевые элементы.
LaTeX
$$$val(K,v,O,hv,p)(f) = 0 \iff f = 0$$$
Lean4
theorem map_eq_zero {f : PreTilt O p} : val K v O hv p f = 0 ↔ f = 0 :=
by
by_cases hf0 : f = 0
· rw [hf0]; exact iff_of_true (Valuation.map_zero _) rfl
obtain ⟨n, hn⟩ : ∃ n, coeff _ _ n f ≠ 0 := not_forall.1 fun h => hf0 <| Perfection.ext h
change valAux K v O p f = 0 ↔ f = 0; refine iff_of_false (fun hvf => hn ?_) hf0
rw [valAux_eq hv hn] at hvf; replace hvf := pow_eq_zero hvf; rwa [ModP.preVal_eq_zero hv] at hvf
