valuation_lt_one_iff_dvd — Mathlib

English

Let R be a Dedekind domain and v a height-one valuation on its fraction field K. For every r in R, the v-adic valuation of r (in K) is strictly less than 1 if and only if the ideal v.asIdeal divides the principal ideal generated by r, i.e. (r).

Русский

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

LaTeX

$$$v.valuation_K(r) < 1 \iff v.asIdeal \mid \operatorname{span}\{r\}$$$

Lean4

/-- The `v`-adic valuation of `r ∈ R` is less than 1 if and only if `v` divides the ideal `(r)`. -/
theorem valuation_lt_one_iff_dvd (r : R) : v.valuation K r < 1 ↔ v.asIdeal ∣ Ideal.span { r } := by
  rw [valuation_of_algebraMap]; exact v.intValuation_lt_one_iff_dvd r

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