Theorems · Definition · ring theory

CliffordAlgebra.changeForm

{R : Type u1} →
  [inst : CommRing R] →
    {M : Type u2} →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          {Q Q' : QuadraticForm R M} →
            {B : LinearMap.BilinForm R M} →
              LinearMap.BilinMap.toQuadraticMap B = Q' - Q → CliffordAlgebra Q →ₗ[R] CliffordAlgebra Q'

Convert between two algebras of different quadratic forms, sending vectors to vectors, scalars to scalars, and adjusting products by a contraction term. This is $\lambda_B$ from [bourbaki2007] §9 Lemma 2.

Defined in

Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Cited by

12 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModule