Q — Mathlib · SciLib

English

Let Q c1 c2 be the quadratic form on R×R given by Q((a,b)) = (c1 a^2, c2 b^2); the corresponding Clifford algebra encodes quaternions with parameters c1, c2.

Русский

Пусть Q c1 c2 — квадратичная форма на R×R, Q((a,b)) = (c1 a^2, c2 b^2); соответствующая клиффордова алгебра кодирует кватернионы с параметрами c1, c2.

LaTeX

$$$Q : \operatorname{QuadraticForm} R (R \times R) := (c_1 \cdot \operatorname{sq}).prod (c_2 \cdot \operatorname{sq})$$$

Lean4

/-- `Q c₁ c₂` is a quadratic form over `R × R` such that `CliffordAlgebra (Q c₁ c₂)` is isomorphic
as an `R`-algebra to `ℍ[R,c₁,c₂]`. -/
def Q : QuadraticForm R (R × R) :=
  (c₁ • QuadraticMap.sq).prod (c₂ • QuadraticMap.sq)

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