Theorems · Theorem · ring theory

CliffordAlgebra.contractRight_eq

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

Defined in

Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModule