intValuation_ne_zero — Mathlib

English

Nonzero elements have nonzero valuation: if x ≠ 0 then v.intValuation x ≠ 0.

Русский

Не нулевые элементы имеют ненулевую оценку: если x ≠ 0, то v.intValuation x ≠ 0.

LaTeX

$$x \neq 0 \Rightarrow v(x) \neq 0$$

Lean4

/-- Nonzero elements have nonzero adic valuation. -/
theorem intValuation_ne_zero (x : R) (hx : x ≠ 0) : v.intValuation x ≠ 0 :=
  by
  rw [v.intValuation_if_neg hx]
  exact WithZero.coe_ne_zero

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