English
The v-adic valuation of r ∈ R is less than 1 iff v.asIdeal divides the ideal (r).
Русский
v-адическая оценка элемента r меньше единицы тогда и только тогда, когда v.asIdeal делит идеал (r).
LaTeX
$$v.intValuation(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 intValuation_lt_one_iff_dvd (r : R) : v.intValuation r < 1 ↔ v.asIdeal ∣ Ideal.span { r } := by
classical
by_cases hr : r = 0
· simp [hr]
· rw [v.intValuation_if_neg hr, ← WithZero.coe_one, ← ofAdd_zero, WithZero.coe_lt_coe, ofAdd_lt, neg_lt_zero, ←
Int.ofNat_zero, Int.ofNat_lt, zero_lt_iff]
have h : (Ideal.span { r } : Ideal R) ≠ 0 :=
by
rw [Ne, Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot]
exact hr
apply Associates.count_ne_zero_iff_dvd h (by apply v.irreducible)