instNormedDivisionRingReal — Mathlib

English

The quaternion algebra ℍ over ℝ is a normed division ring: the norm is multiplicative, ∥xy∥ = ∥x∥ ∥y∥ for all x,y ∈ ℍ.

Русский

Кватернионная алгебра ℍ над ℝ является нормированным дивизионным кольцом: норма умножения, ∥xy∥ = ∥x∥ ∥y∥ для всех x,y ∈ ℍ.

LaTeX

$$$\\forall x,y \\in \\mathbb{H},\\quad \\|xy\\| = \\|x\\| \\cdot \\|y\\|.$$$

Lean4

noncomputable instance : NormedDivisionRing ℍ where
  dist_eq _ _ := rfl
  norm_mul _ _ := by simp [norm_eq_sqrt_real_inner, inner_self]

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