Theorems · Definition · linear algebra

CliffordAlgebra.toProd

{R : Type u_1} →
  {M₁ : Type u_2} →
    {M₂ : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M₁] →
          [inst_2 : AddCommGroup M₂] →
            [inst_3 : Module R M₁] →
              [inst_4 : Module R M₂] →
                (Q₁ : QuadraticForm R M₁) →
                  (Q₂ : QuadraticForm R M₂) →
                    GradedTensorProduct R (CliffordAlgebra.evenOdd Q₁) (CliffordAlgebra.evenOdd Q₂) →ₐ[R]
                      CliffordAlgebra (QuadraticMap.prod Q₁ Q₂)

The reverse direction of CliffordAlgebra.prodEquiv.

Defined in

Mathlib.LinearAlgebra.CliffordAlgebra.Prod

Cited by

5 results in Mathlib

Foundations

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

Assumes

CommRingAddCommGroupAddCommGroupModuleModule