instCStarRingReal — Mathlib

English

The quaternions ℍ over ℝ form a C*-ring (indeed a C*-algebra), satisfying the C*-identity ∥x* x∥ = ∥x∥^2 for all x ∈ ℍ.

Русский

Кватернионы ℍ над ℝ образуют C*-кольцо (на самом деле C*-алгебру), удовлетворяющее C*-неравенству ∥x* x∥ = ∥x∥^2 для всех x ∈ ℍ.

LaTeX

$$$\\forall x \\in \\mathbb{H},\\quad \\|x^{*} x\\| = \\|x\\|^{2}.$$$

Lean4

instance : CStarRing ℍ where
  norm_mul_self_le x := le_of_eq <| Eq.symm <| (norm_mul _ _).trans <| congr_arg (· * ‖x‖) (norm_star x)

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