frobenius_norm_conjTranspose — Mathlib

English

The Frobenius norm is invariant under conjugation: ∥Aᴴ∥ = ∥A∥.

Русский

Норма Фробениуса инвариантна по отношению к сопряжённому транспонированию: ∥Aᴴ∥ = ∥A∥.

LaTeX

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

Lean4

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

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