Theorems · Theorem · ring theory

CliffordAlgebra.contractRight_comm

∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (d d' : Module.Dual R M) (x : CliffordAlgebra Q),
  (CliffordAlgebra.contractRight ((CliffordAlgebra.contractRight x) d)) d' =
    -(CliffordAlgebra.contractRight ((CliffordAlgebra.contractRight x) d')) d

This is [grinberg_clifford_2016] Theorem 14

Defined in

Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Cited by

0 results in Mathlib

Foundations

Depth 112 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingAddCommGroupModule