valuation_coe — Mathlib

English

The real-valued coercion of the valuation equals the usual norm: ((Valued.v x : ℝ≥0) : ℝ) = ||x||.

Русский

Приведение значения величины к действительному числу сохраняет норму: ((v x) : ℝ) = ||x||.

LaTeX

$$$$\bigl((\operatorname{Valued.v} x : \mathbb{R}_{\ge 0}) : \mathbb{R}\bigr) = \|x\|.$$$$

Lean4

/-- The coercion of the valuation of `x : PadicAlgCl p` to `ℝ` agrees with its norm. -/
@[simp]
theorem valuation_coe (x : PadicAlgCl p) : ((Valued.v x : ℝ≥0) : ℝ) = ‖x‖ :=
  rfl

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