toComplex_ι

Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

URI: https://scilib.ai/kg/mathlib#CliffordAlgebraComplex.toComplex_ι

English

The image of the complex unit i under the ofComplex map is the generator ι_Q 1 in CliffordAlgebra Q.

Русский

Образ единицы i в ℂ под отображением toComplex равен генератору ι_Q 1 в CliffordAlgebra(Q).

LaTeX

$$$\operatorname{toComplex}(\mathbf{i}) = \iota_Q(1)$$$

Lean4

@[simp]
theorem toComplex_ι (r : ℝ) : toComplex (ι Q r) = r • Complex.I :=
  CliffordAlgebra.lift_ι_apply _ _ r

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

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

Разделы

Аффилиация

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