valuation_eq_intValuationDef — Mathlib

English

The valuation on K agrees with intValuationDef when restricted to R: for r ∈ R, valuation_K r = intValuationDef r.

Русский

Оценка на K совпадает с intValuationDef при ограничении к R: для r ∈ R, valuation_K(r) = intValuationDef(r).

LaTeX

$$v.valuation K r = v.intValuationDef r$$

Lean4

@[deprecated valuation_of_algebraMap (since := "2025-05-11")]
theorem valuation_eq_intValuationDef (r : R) : v.valuation K r = v.intValuationDef r :=
  Valuation.extendToLocalization_apply_map_apply ..

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