v_p_lt_preVal — Mathlib

English

For x ∈ ModP O p, v p < preVal(x) iff x ≠ 0.

Русский

Для x ∈ ModP O p: v p < preVal(x) тогда и только тогда, когда x ≠ 0.

LaTeX

$$$v(p) < \mathrm{preVal}(x) \iff x \neq 0$$$

Lean4

theorem v_p_lt_preVal {x : ModP O p} : v p < preVal K v O p x ↔ x ≠ 0 :=
  by
  refine ⟨fun h hx => by rw [hx, preVal_zero] at h; exact not_lt_zero' h, fun h => lt_of_not_ge fun hp => h ?_⟩
  obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective x
  rw [preVal_mk hv h, ← map_natCast (algebraMap O K) p, hv.le_iff_dvd] at hp
  · rw [Ideal.Quotient.eq_zero_iff_mem, Ideal.mem_span_singleton]; exact hp

Похожие утверждения