abs_norm_eq_max_natAbs — Mathlib

English

For every natural n, the norm of the vector (1, n+1) equals n+1, i.e. ∥![1,(n+1)]∥ = n+1 with the standard max-norm.

Русский

Для каждого натурального n норма вектора (1, n+1) равна n+1; то есть ∥(1, n+1)∥ = n+1.

LaTeX

$$$\|\![1, (n + 1)\!\]\| = n + 1$$$

Lean4

theorem abs_norm_eq_max_natAbs (n : ℕ) : ‖![1, (n + 1 : ℤ)]‖ = n + 1 :=
  by
  simp only [EisensteinSeries.norm_eq_max_natAbs, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_fin_one]
  norm_cast
  simp

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