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