toAbsoluteValue — Mathlib

English

The norm on a NormedField can be viewed as an AbsoluteValue on the underlying ring.

Русский

Норма на нормированном поле может рассматриваться как абсолютная величина на базовом кольце.

LaTeX

$$$(\text{NormedField.toAbsoluteValue } R) : \text{AbsoluteValue } R \mathbb{R}$$$

Lean4

/-- The norm on a `NormedField`, as an `AbsoluteValue`. -/
def toAbsoluteValue (R : Type*) [NormedField R] : AbsoluteValue R ℝ
    where
  toFun := norm
  map_mul' := norm_mul
  nonneg' := norm_nonneg
  eq_zero' _ := norm_eq_zero
  add_le' := norm_add_le

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