instHasSolidNormRat — Mathlib

English

The rational numbers ℚ carry a solid norm, given by the standard absolute value via the usual embedding into the reals.

Русский

Рациональные числа ℚ обладают солидной нормой; норма определяется модулем через естественное вложение в ℝ.

LaTeX

$$$\text{HasSolidNorm } \mathbb{Q}$$$

Lean4

instance : HasSolidNorm ℚ :=
  ⟨fun _ _ _ => by simpa only [norm, ← Rat.cast_abs, Rat.cast_le]⟩

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