Q' — Mathlib · SciLib

English

The Q' construction provides a canonical polynomial-like map giving a Clifford algebra of a product form.

Русский

Конструкция Q' задаёт каноническое отображение, связывающее CliffordAlgebra с произведением форм.

LaTeX

$$Q' : QuadraticForm R (M) -> QuadraticForm R (M×R)$$

Lean4

/-- The quadratic form on the augmented vector space `M × R` sending `v + r•e0` to `Q v - r^2`. -/
abbrev Q' : QuadraticForm R (M × R) :=
  Q.prod <| -QuadraticMap.sq (R := R)

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