intValuation_lt_one_iff_mem — Mathlib

English

The valuation is less than 1 exactly when r lies in the ideal v.asIdeal.

Русский

Оценка меньше единицы тогда, когда r принадлежит идеалу v.asIdeal.

LaTeX

$$v.intValuation(r) < 1 \iff r \in v.asIdeal$$

Lean4

/-- The `v`-adic valuation of `r ∈ R` is less than 1 if and only if `r ∈ v`. -/
theorem intValuation_lt_one_iff_mem (r : R) : v.intValuation r < 1 ↔ r ∈ v.asIdeal := by
  rw [intValuation_lt_one_iff_dvd, Ideal.dvd_span_singleton]

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