aux — Mathlib

English

The Clifford algebra over 0 forms is isomorphic to dual numbers, via a canonical AlgEquiv.

Русский

Клиффордова алгебра над нулевой квадратичной формой изоморфна дуальным числам через каноническое AlgEquiv.

LaTeX

$$equiv: CliffordAlgebra (0) ≃ₐ[R] R[ε]$$

Lean4

/-- The final auxiliary construction for `CliffordAlgebra.even.lift`. This map is the forwards
direction of that equivalence, but not in the fully-bundled form. -/
@[simps! -isSimp apply]
def aux (f : EvenHom Q A) : CliffordAlgebra.even Q →ₗ[R] A :=
  by
  refine ?_ ∘ₗ (even Q).val.toLinearMap
  exact LinearMap.fst R _ _ ∘ₗ foldr Q (fFold f) (fFold_fFold f) (1, 0)

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