reverse_e0

Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv

URI: https://scilib.ai/kg/mathlib#CliffordAlgebra.EquivEven.reverse_e0

English

The reverse of the new-dimension unit vector equals itself: reverse(e0(Q)) = e0(Q).

Русский

Обратная к единичному вектору новой размерности равна самому вектору: reverse(e0(Q)) = e0(Q).

LaTeX

$$$\text{reverse}(e_0(Q)) = e_0(Q)$$$

Lean4

@[simp]
theorem reverse_e0 : reverse (Q := Q' Q) (e0 Q) = e0 Q :=
  reverse_ι _

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

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

Разделы

Аффилиация

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