English
Let R be a commutative ring and M an R-module with a quadratic form Q. For any duals d, d' ∈ Module.Dual(R, M) and any x in the Clifford algebra Cl(Q), the successive right contractions satisfy x ⌊ d ⌊ d' = - x ⌊ d' ⌊ d.
Русский
Пусть R — коммутативное кольцо, M — модуль над R с квадратичной формой Q. Для любых двойственных элементов d, d' ∈ Module.Dual(R, M) и любого x ∈ клИффордова алгебра Cl(Q) выполняется x ⌊ d ⌊ d' = - x ⌊ d' ⌊ d.
LaTeX
$$$\bigl(\text{contractRight}_d(\text{contractRight}_{d'}(x))\bigr) = -\bigl(\text{contractRight}_{d'}(\text{contractRight}_d(x))\bigr)$$$
Lean4
/-- This is [grinberg_clifford_2016][] Theorem 14 -/
theorem contractRight_comm (x : CliffordAlgebra Q) : x⌊d⌊d' = -(x⌊d'⌊d) := by
rw [contractRight_eq, contractRight_eq, contractRight_eq, contractRight_eq, reverse_reverse, reverse_reverse,
contractLeft_comm, map_neg]
/- TODO:
lemma contractRight_contractLeft (x : CliffordAlgebra Q) : (d ⌋ x) ⌊ d' = d ⌋ (x ⌊ d') :=
-/
