CliffordAlgebra — Mathlib

English

For an R-module M with a quadratic form Q, there is a universal algebra encapsulating the relations v^2 = Q(v) for v ∈ M, forming the Clifford algebra Cl(Q).

Русский

Для R-модуля M с квадратично формой Q существует универсальная алгебра, задающая отношения v^2 = Q(v) для всех v ∈ M, называемая клиффордовой алгеброй Cl(Q).

LaTeX

$$CliffordAlgebra(Q)$$

Lean4

/-- The Clifford algebra of an `R`-module `M` equipped with a quadratic_form `Q`.
-/
def CliffordAlgebra :=
  RingQuot (CliffordAlgebra.Rel Q)
deriving Inhabited, Ring, Algebra R

Похожие утверждения