intValuation_le_pow_iff_dvd — Mathlib

English

v.intValuation r ≤ ofAdd(-n) iff v.asIdeal^n divides (r).

Русский

v.intValuation(r) ≤ -n тогда и только тогда, когда v.asIdeal^n делит (r).

LaTeX

$$v.intValuation(r) \le \operatorname{ofAdd}(-n) \iff v.asIdeal^n \mid \operatorname{span}\{r\}$$

Lean4

/-- The `v`-adic valuation of `r ∈ R` is less than `Multiplicative.ofAdd (-n)` if and only if
`vⁿ` divides the ideal `(r)`. -/
theorem intValuation_le_pow_iff_dvd (r : R) (n : ℕ) :
    v.intValuation r ≤ Multiplicative.ofAdd (-(n : ℤ)) ↔ v.asIdeal ^ n ∣ Ideal.span { r } := by
  classical
  by_cases hr : r = 0
  · simp_rw [hr, Valuation.map_zero, Ideal.dvd_span_singleton, zero_le', Submodule.zero_mem]
  ·
    rw [v.intValuation_if_neg hr, WithZero.coe_le_coe, ofAdd_le, neg_le_neg_iff, Int.ofNat_le, Ideal.dvd_span_singleton,
      ← Associates.le_singleton_iff,
      Associates.prime_pow_dvd_iff_le (Associates.mk_ne_zero'.mpr hr) (by apply v.associates_irreducible)]

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