norm_diagonal

Mathlib.Analysis.Matrix

URI: https://scilib.ai/kg/mathlib#Matrix.norm_diagonal

English

For any v: n → α, the norm of diagonal v equals the norm of v: ∥diagonal v∥ = ∥v∥.

Русский

Для любого v: n → α норма диагональной матрицы равна норме вектора: ∥diagonal v∥ = ∥v∥.

LaTeX

$$$\|\text{diagonal } v\| = \|v\|.$$$

Lean4

@[simp]
theorem norm_diagonal [DecidableEq n] (v : n → α) : ‖diagonal v‖ = ‖v‖ :=
  congr_arg ((↑) : ℝ≥0 → ℝ) <| nnnorm_diagonal v

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru