norm_conjTranspose

Mathlib.Analysis.Matrix

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

← MathLib Explorer

English

For any A, nnnorm of the conjugate transpose equals nnnorm of A: ∥Aᴴ∥₊ = ∥A∥₊.

Русский

Для любой матрицы верно: nnnorm(Aᴴ) = nnnorm(A).

LaTeX

$$$\|A^H\|_+ = \|A\|_+.$$$

Lean4

@[simp]
theorem norm_conjTranspose [StarAddMonoid α] [NormedStarGroup α] (A : Matrix m n α) : ‖Aᴴ‖ = ‖A‖ :=
  congr_arg ((↑) : ℝ≥0 → ℝ) <| nnnorm_conjTranspose A

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

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

Разделы

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

Аффилиация

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