Q_apply

Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

URI: https://scilib.ai/kg/mathlib#CliffordAlgebraComplex.Q_apply

English

For every real r, the image of ι_Q r under toComplex is r times the imaginary unit i.

Русский

Для каждого вещественного r образ ι_Q r при отображении toComplex равен r на мнимую единицу i.

LaTeX

$$$\operatorname{toComplex}(\iota\,Q\, r) = r \cdot \mathsf{I}$$$

Lean4

@[simp]
theorem Q_apply (r : ℝ) : Q r = -(r * r) :=
  rfl

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

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

Разделы

Аффилиация

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