instNormedAlgebraReal — Mathlib

English

The quaternion algebra ℍ over ℝ forms a Normed Algebra, i.e., the norm is compatible with scalar multiplication: ∥λx∥ ≤ |λ| ∥x∥ for all λ ∈ ℝ, x ∈ ℍ.

Русский

Кватернионная алгебра ℍ над ℝ образует нормированную алгебру: норма совместима с умножением на скаляры: ∥λx∥ ≤ |λ| ∥x∥, для всех λ ∈ ℝ, x ∈ ℍ.

LaTeX

$$$\\forall \\lambda \\in \\mathbb{R},\\; \\forall x \\in \\mathbb{H},\\quad \\|\\lambda x\\| \\le |\\lambda| \\|x\\|.$$$

Lean4

noncomputable instance : NormedAlgebra ℝ ℍ
    where
  norm_smul_le := norm_smul_le
  toAlgebra := Quaternion.algebra

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