nnnorm_transpose

Mathlib.Analysis.Matrix

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

English

The norm is invariant under transpose: ∥A^T∥ = ∥A∥.

Русский

Норма сохраняется при транспонировании: ∥A^T∥ = ∥A∥.

LaTeX

$$$\|A^T\| = \|A\|.$$$

Lean4

@[simp]
theorem nnnorm_transpose (A : Matrix m n α) : ‖Aᵀ‖₊ = ‖A‖₊ :=
  Finset.sup_comm _ _ _

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

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

Разделы

Аффилиация

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