Theorems · Theorem · ring theory

CliffordAlgebra.contractLeft_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.contractLeft d) ((CliffordAlgebra.contractLeft d') x) =
    -(CliffordAlgebra.contractLeft d') ((CliffordAlgebra.contractLeft d) x)

This is [grinberg_clifford_2016] Theorem 8

Defined in

Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModule