Theorems · Definition · ring theory

CliffordAlgebra.changeFormEquiv

{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'

Any two algebras whose quadratic forms differ by a bilinear form are isomorphic as modules. This is $\bar \lambda_B$ from [bourbaki2007] §9 Proposition 3.

Defined in

Mathlib.LinearAlgebra.CliffordAlgebra.Contraction

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupModule