Theorems · Theorem · ring theory

CliffordAlgebra.contractLeftAux_apply_apply

∀ {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) (a : M) (a_1 : CliffordAlgebra Q × CliffordAlgebra Q),
  ((CliffordAlgebra.contractLeftAux Q d) a) a_1 = d a • a_1.1 - (CliffordAlgebra.ι Q) a * a_1.2

Defined in

Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Cited by

2 results in Mathlib

Foundations

Depth 59 from the axioms · uses propext, Quot.sound

Assumes

CommRingAddCommGroupModule