preVal_eq_zero — Mathlib

English

The comparison between v(p) and v(algebraMap_O_K x) is equivalent to (Ideal.Quotient.mk x) ≠ 0 in ModP O p.

Русский

Сравнение v(p) и v(algebraMap_O_K x) эквивалентно тому, что (Ideal.Quotient.mk x) ≠ 0 в ModP O p.

LaTeX

$$$v(p) < v(\text{algebraMap}_O^K(x)) \iff (\mathrm{Ideal.Quotient.mk} _ x : \mathrm{ModP}(O,p)) \neq 0$$$

Lean4

theorem preVal_eq_zero {x : ModP O p} : preVal K v O p x = 0 ↔ x = 0 :=
  ⟨fun hvx =>
    by_contradiction fun hx0 : x ≠ 0 => by
      rw [← v_p_lt_preVal (hv := hv), hvx] at hx0
      exact not_lt_zero' hx0,
    fun hx => hx.symm ▸ preVal_zero⟩

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