intValuation_le_pow_iff_mem — Mathlib

English

v.intValuation r ≤ -n iff r ∈ v.asIdeal^n.

Русский

v.intValuation(r) ≤ -n эквивалентно r ∈ v.asIdeal^n.

LaTeX

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

Lean4

/-- The `v`-adic valuation of `r ∈ R` is less than `Multiplicative.ofAdd (-n)` if and only if
`r ∈ vⁿ`. -/
theorem intValuation_le_pow_iff_mem (r : R) (n : ℕ) :
    v.intValuation r ≤ Multiplicative.ofAdd (-(n : ℤ)) ↔ r ∈ v.asIdeal ^ n := by
  rw [intValuation_le_pow_iff_dvd, Ideal.dvd_span_singleton]

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