valuation_of_mk' — Mathlib

English

The v-adic valuation of r is ≤ -(n) iff v.asIdeal^n divides (r).

Русский

v-адическая оценка r не превосходит -(n) тогда и только тогда, когда v.asIdeal^n делит (r).

LaTeX

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

Lean4

/-- The `v`-adic valuation of `r/s ∈ K` is the valuation of `r` divided by the valuation of `s`. -/
theorem valuation_of_mk' {r : R} {s : nonZeroDivisors R} :
    v.valuation K (IsLocalization.mk' K r s) = v.intValuation r / v.intValuation s := by
  rw [valuation_def, Valuation.extendToLocalization_mk', div_eq_mul_inv]

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