reverse_v

Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv

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

English

The reverse operation fixes the image of v: reverse(v(Q)m) = v(Q)m.

Русский

Обратная операция сохраняет образ v: reverse(v(Q)m) = v(Q)m.

LaTeX

$$$\text{reverse}(v_Q(m)) = v_Q(m)$$$

Lean4

@[simp]
theorem reverse_v (m : M) : reverse (Q := Q' Q) (v Q m) = v Q m :=
  reverse_ι _

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

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

Разделы

Аффилиация

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