norm_eq_abv — Mathlib

English

For any Ring R, a real-valued absolute value v, and x in WithAbs v, the norm of x equals v applied to the corresponding element in R via the canonical equivalence.

Русский

Для каждого кольца R, вещественного абсолютного значения v и x ∈ WithAbs v нормa x равна v применённому к соответствующему элементу в R через каноническое эквивалентное отображение.

LaTeX

$$$\\|x\\| = v(\\mathrm{WithAbs}(v)\\!\\text{-equiv}(x))$$$

Lean4

theorem norm_eq_abv [Ring R] (v : AbsoluteValue R ℝ) (x : WithAbs v) : ‖x‖ = v (WithAbs.equiv v x) :=
  rfl

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