frobenius_normedStarGroup — Mathlib

English

There is a NormedStarGroup structure on Matrix m m α induced by the Frobenius norm, i.e., the star operation is isometric under the Frobenius norm.

Русский

Матрицы размером m×m над α образуют NormedStarGroup посредством нормы Фробениуса; операция сопряжения сохраняет норму.

LaTeX

$$$\text{NormedStarGroup}(\mathrm{Matrix}_{m\times m}(\alpha))$ with Frobenius norm; $\|A^*\| = \|A\|$.$$

Lean4

instance frobenius_normedStarGroup [StarAddMonoid α] [NormedStarGroup α] : NormedStarGroup (Matrix m m α) :=
  ⟨(le_of_eq <| frobenius_norm_conjTranspose ·)⟩

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