Theorems · Theorem · ring theory

CliffordAlgebra.contractLeft_algebraMap_mul

∀ {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) (r : R) (b : CliffordAlgebra Q),
  (CliffordAlgebra.contractLeft d) ((algebraMap R (CliffordAlgebra Q)) r * b) =
    (algebraMap R (CliffordAlgebra Q)) r * (CliffordAlgebra.contractLeft d) b

Defined in

Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModule