neg_v_mul_e0

Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv

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

English

Equivalently, the product v(m) e0 equals minus e0 v(m): −(v(m) · e0) = e0 · v(m).

Русский

Равносильно: произведение v(m) e0 равно минус e0 v(m).

LaTeX

$$$-(v_Q(m) \\cdot e_0(Q)) = e_0(Q) \\cdot v_Q(m)$$$

Lean4

theorem neg_v_mul_e0 (m : M) : -(v Q m * e0 Q) = e0 Q * v Q m :=
  by
  rw [neg_eq_iff_eq_neg]
  exact (neg_e0_mul_v _ m).symm

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

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

Разделы

Аффилиация

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