nnnorm_conjTranspose — Mathlib

English

The collection of square matrices over a normed star group α forms a NormedStarGroup structure.

Русский

Набор квадратных матриц над нормированной звездной группой α образует структуру NormedStarGroup.

LaTeX

$$$\text{NormedStarGroup}(\text{Matrix } m\, m\, α).$$$

Lean4

@[simp]
theorem nnnorm_conjTranspose [StarAddMonoid α] [NormedStarGroup α] (A : Matrix m n α) : ‖Aᴴ‖₊ = ‖A‖₊ :=
  (nnnorm_map_eq _ _ nnnorm_star).trans A.nnnorm_transpose

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