frobenius_nnnorm_transpose

Mathlib.Analysis.Matrix

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

← MathLib Explorer

English

The NN-norm of the conjugate transpose Aᴴ equals the NN-norm of A.

Русский

NN-норма сопряжённого транспонирования Aᴴ равна NN-норме A.

LaTeX

$$$\|A^{\mathrm{H}}\|_{NN} = \|A\|_{NN}.$$$

Lean4

@[simp]
theorem frobenius_nnnorm_transpose (A : Matrix m n α) : ‖Aᵀ‖₊ = ‖A‖₊ :=
  by
  rw [frobenius_nnnorm_def, frobenius_nnnorm_def, Finset.sum_comm]
  simp_rw [Matrix.transpose_apply]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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