contractLeft_contractLeft — Mathlib

English

For any x in Clifford(Q) there holds d ⌋ (d ⌋ x) = 0; applying left contraction twice yields zero.

Русский

Для любого x в Clifford(Q) выполнено d ⌋ (d ⌋ x) = 0; дважды подряд применённое левое свёртывание даёт ноль.

LaTeX

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

Lean4

/-- This is [grinberg_clifford_2016][] Theorem 7 -/
theorem contractLeft_contractLeft (x : CliffordAlgebra Q) : d⌋(d⌋x) = 0 := by
  induction x using CliffordAlgebra.left_induction with
  | algebraMap => simp_rw [contractLeft_algebraMap, map_zero]
  | add _ _ hx hy => rw [map_add, map_add, hx, hy, add_zero]
  | ι_mul _ _ hx =>
    rw [contractLeft_ι_mul, map_sub, contractLeft_ι_mul, hx, LinearMap.map_smul, mul_zero, sub_zero, sub_self]

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