instNormedAddCommGroup — Mathlib

English

The additive group of integers ℤ is equipped with a norm defined by the absolute value via its real embedding, so ∥n∥ = |n| and the induced metric is d(m,n) = |m−n|.

Русский

Целые числа ℤ образуют нормированную аддитивную группу, нормa задаётся как модуль через вложение в ℝ: ∥n∥ = |n|, а расстояние d(m,n) = |m−n|.

LaTeX

$$$\|n\| = |n|$$$

Lean4

instance instNormedAddCommGroup : NormedAddCommGroup ℤ
    where
  norm n := ‖(n : ℝ)‖
  dist_eq m n := by simp only [Int.dist_eq, norm, Int.cast_sub]

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