Theorems · Definition · linear algebra

CliffordAlgebra.toBaseChange

{R : Type u_1} →
  (A : Type u_2) →
    {V : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : CommRing A] →
          [inst_2 : AddCommGroup V] →
            [inst_3 : Algebra R A] →
              [inst_4 : Module R V] →
                [inst_5 : Invertible 2] →
                  (Q : QuadraticForm R V) →
                    CliffordAlgebra (QuadraticForm.baseChange A Q) →ₐ[A] TensorProduct R A (CliffordAlgebra Q)

Convert from the clifford algebra over a base-changed module to the base-changed clifford algebra.

Defined in

Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange

Cited by

10 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAddCommGroupAlgebraModuleInvertible