intValuation_lt_one_iff_dvd — Mathlib

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)

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