instInnerProductSpaceReal — Mathlib

English

The quaternions over the real numbers can be equipped with a real-valued inner product, turning ℍ into a real inner product space.

Русский

Кватернионы над ℝ можно наделить вещественным скалярным произведением, превращая ℍ в вещественное пространство скалярного произведения.

LaTeX

$$$(\\mathbb{H},\\langle\\cdot,\\cdot\\rangle)$ is a real inner product space.$$

Lean4

noncomputable instance : InnerProductSpace ℝ ℍ :=
  InnerProductSpace.ofCore _

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