inner_def

Mathlib.Analysis.Quaternion

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

English

The real inner product on ℍ is given by ⟪a,b⟫ = (a · conj(b)).re.

Русский

Реальное внутренняя скалярное произведение на ℍ задаётся как ⟪a,b⟫ = Re(a · conj(b)).

LaTeX

$$$$ \\langle a,b \\rangle = \\operatorname{Re}(a \\cdot \\overline{b}). $$$$

Lean4

theorem inner_def (a b : ℍ) : ⟪a, b⟫ = (a * star b).re :=
  rfl

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

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

Разделы

Аффилиация

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