Theorems · Definition · ring theory

CliffordAlgebra.contractLeft

{R : Type u1} →
  [inst : CommRing R] →
    {M : Type u2} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {Q : QuadraticForm R M} → Module.Dual R M →ₗ[R] CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q

Contract an element of the Clifford algebra with an element d : Module.Dual R M from the left. Note that $v ⌋ x$ is spelt contractLeft (Q.associated v) x. This includes [grinberg_clifford_2016] Theorem 10.75

Defined in

Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Cited by

22 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModule