valuation_lt_one_iff_mem — Mathlib

English

Let R be a Dedekind domain and v a height-one spectrum point. For any r in R, v-valuation r is less than 1 if and only if r belongs to the ideal v.asIdeal.

Русский

Пусть R — область Дедекдина и v — точка в спектре высоты единицы. Для любого r ∈ R v-оценка r меньше 1 тогда и только тогда, когда r принадлежит идеалу v.asIdeal.

LaTeX

$$$\forall r\in R,\ v.valuation_K(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 valuation_lt_one_iff_mem (r : R) : v.valuation K r < 1 ↔ r ∈ v.asIdeal := by rw [valuation_of_algebraMap];
  exact v.intValuation_lt_one_iff_mem r

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