e0_mul_v_mul_e0

Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv

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

← MathLib Explorer

English

Conjugating v(m) by e0 leaves v(m) invariant: e0 · v(m) · e0 = v(m).

Русский

Сопряжение v(m) элементом e0 сохраняет v(m): e0 · v(m) · e0 = v(m).

LaTeX

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

Lean4

@[simp]
theorem e0_mul_v_mul_e0 (m : M) : e0 Q * v Q m * e0 Q = v Q m := by
  rw [← neg_v_mul_e0, ← neg_mul, mul_assoc, e0_mul_e0, mul_neg_one, neg_neg]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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