ofComplex_I

Mathlib.LinearAlgebra.CliffordAlgebra.Equivs

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

English

The image of the complex unit i under ofComplex equals ι Q 1.

Русский

Образ единицы i в ℂ под ofComplex равен ι_Q 1.

LaTeX

$$$\operatorname{ofComplex}(\mathsf{i}) = \iota_Q(1)$$$

Lean4

@[simp]
theorem ofComplex_I : ofComplex Complex.I = ι Q 1 :=
  Complex.liftAux_apply_I _ (by simp)

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

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

Разделы

Аффилиация

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