instNormedField — Mathlib

English

The rational numbers ℚ form a NormedField with the standard absolute-value norm.

Русский

Числа рациональные ℚ образуют нормированное поле с обычной нормой по абсолютной величине.

LaTeX

$$$\text{NormedField}(\mathbb{Q})$ with $\|q\| = |q|$.$$

Lean4

instance instNormedField : NormedField ℚ where
  __ := instField
  __ := instNormedAddCommGroup
  norm_mul a b := by simp only [norm, Rat.cast_mul, abs_mul]

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