Theorems · Definition · ring theory

CliffordAlgebra

{R : Type u_1} →
  [inst : CommRing R] →
    {M : Type u_2} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → QuadraticForm R M → Type (max u_1 u_2)

The Clifford algebra of an R-module M equipped with a QuadraticForm Q.

Defined in

Mathlib.LinearAlgebra.CliffordAlgebra.Basic

Cited by

309 results in Mathlib

Foundations

Depth 40 from the axioms, rests on 437 definitions · uses propext, Quot.sound

Assumes

CommRingAddCommGroupModule