valuation_of_algebraMap — Mathlib

English

The v-adic valuation on K extends the v-adic valuation on R: for r ∈ R, valuation_K(r) = intValuation(r).

Русский

v-адическая оценка на K распространяется на R: для r ∈ R valuation_K(r) = intValuation(r).

LaTeX

$$v.valuation K r = v.intValuation r$$

Lean4

/-- The `v`-adic valuation on `K` extends the `v`-adic valuation on `R`. -/
theorem valuation_of_algebraMap (r : R) : v.valuation K r = v.intValuation r := by
  rw [valuation_def, Valuation.extendToLocalization_apply_map_apply]

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