abs_norm_eq_max_natAbs_neg — Mathlib

English

Similarly, the norm of the vector (1, −(n+1)) equals n+1, i.e. ∥![1, −(n+1)]∥ = n+1.

Русский

Аналогично, норма вектора (1, −(n+1)) равна n+1; то есть ∥(1, −(n+1))∥ = n+1.

LaTeX

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

Lean4

theorem abs_norm_eq_max_natAbs_neg (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

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