instInnerReal

Mathlib.Analysis.Quaternion

URI: https://scilib.ai/kg/mathlib#Quaternion.instInnerReal

English

The real quaternions ℍ are equipped with the real inner product ⟪a,b⟫ = Re(a·conj(b)).

Русский

Кватернионы ℍ оснащены вещественным скалярным произведением ⟪a,b⟫ = Re(a·conj(b)).

LaTeX

$$$$ \\langle a,b \\rangle = \\Re\\bigl(a \\overline{b}\\bigr). $$$$

Lean4

instance : Inner ℝ ℍ :=
  ⟨fun a b => (a * star b).re⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru