instCStarModule — Mathlib

English

The operator-normed matrix algebra satisfies the C*-property: ∥A* A∥ = ∥A∥^2.

Русский

Алгебра матриц с нормой оператора удовлетворяет C*-свойству: ∥A* A∥ = ∥A∥^2.

LaTeX

$$$\\forall A: M_{n\\times n}(\\mathbb{C}), \\\\ \\|A^{\\ast} A\\|_{2} = \\|A\\|_{2}^{2}$$$

Lean4

/-- Reinterpret a C⋆-algebra `A` as a `CStarModule` over itself. -/
instance : CStarModule A A where
  inner x y := y * star x
  inner_add_right := add_mul ..
  inner_self_nonneg := mul_star_self_nonneg _
  inner_self := CStarRing.mul_star_self_eq_zero_iff _
  inner_op_smul_right := mul_assoc ..
  inner_smul_right_complex := smul_mul_assoc ..
  star_inner x y := by simp
  norm_eq_sqrt_norm_inner_self
    {x} := by
    rw [← sq_eq_sq₀ (norm_nonneg _) (by positivity)]
    simpa [sq] using Eq.symm <| CStarRing.norm_self_mul_star

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