contractRight_contractRight — Mathlib

English

Similarly, contractRight applied twice yields zero: x ⌊ d ⌊ d = 0 for any x.

Русский

Аналогично, правое свёртывание дважды применённое даёт ноль: x ⌊ d ⌊ d = 0.

LaTeX

$$$ x\\lbrack d\\lbrack d = 0 $$$

Lean4

/-- This is [grinberg_clifford_2016][] Theorem 13 -/
theorem contractRight_contractRight (x : CliffordAlgebra Q) : x⌊d⌊d = 0 := by
  rw [contractRight_eq, contractRight_eq, reverse_reverse, contractLeft_contractLeft, map_zero]

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