v — Mathlib · SciLib

English

There is a canonical linear embedding v of the original vector space M into the Clifford algebra of the enlarged form Q' Q, obtained by composing the standard embedding ι with the inclusion of M into M × {0}.

Русский

Существует краевая линейная вложенность v оригинального пространства M в клиффордову алгебру расширенной формы Q' Q, получаемая как композиция нормального вложения ι с включением M в M × {0}.

LaTeX

$$$v_Q(m) = \iota_{Q' Q}(m,0)$$$

Lean4

/-- The embedding from the existing vector space -/
def v : M →ₗ[R] CliffordAlgebra (Q' Q) :=
  ι (Q' Q) ∘ₗ LinearMap.inl _ _ _

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