toClifford_ι

Mathlib.LinearAlgebra.CliffordAlgebra.Basic

URI: https://scilib.ai/kg/mathlib#TensorAlgebra.toClifford_ι

English

The canonical image sends TensorAlgebra.ι_R m to CliffordAlgebra.ι_Q m.

Русский

Каноническое отображение отправляет TensorAlgebra.ι_R m в CliffordAlgebra.ι_Q m.

LaTeX

$$$ toClifford (TensorAlgebra.ι R m) = CliffordAlgebra.ι Q m $$$

Lean4

@[simp]
theorem toClifford_ι (m : M) : toClifford (TensorAlgebra.ι R m) = CliffordAlgebra.ι Q m := by simp [toClifford]

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

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

Разделы

Аффилиация

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