valuation_extends — Mathlib

English

The valuation on ℂ_p extends the valuation on PadicAlgCl(p).

Русский

Оценка на ℂ_p ограничивает и продолжается оценку на PadicAlgCl(p).

LaTeX

$$$v_{\mathbb{C}_p}(x) = v_{\mathrm{PadicAlgCl}_p}(x)\quad(x \in \mathrm{PadicAlgCl}(p)).$$$

Lean4

/-- The valuation on `ℂ_[p]` extends the valuation on `PadicAlgCl p`. -/
theorem valuation_extends (x : PadicAlgCl p) : Valued.v (x : ℂ_[p]) = Valued.v x :=
  Valued.extension_extends _

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