ofComplex — Mathlib

English

There is a canonical ℝ‑algebra homomorphism from ℂ into CliffordAlgebra Q, constructed via Complex.lift sending i to ι Q 1 and preserving the relations.

Русский

Существует тождественный ℝ‑алгебровый гомоморфизм из ℂ в CliffordAlgebra(Q), строящийся через Complex.lift: i ↦ ι Q 1 и сохраняющий отношения.

LaTeX

$$$\operatorname{ofComplex} : \mathbb{C} \to_{\mathbb{R}} \operatorname{CliffordAlgebra}(Q)$$$

Lean4

/-- Intermediate result for `CliffordAlgebraComplex.equiv`: `ℂ` can be converted to
`CliffordAlgebraComplex.Q` above can be converted to. -/
def ofComplex : ℂ →ₐ[ℝ] CliffordAlgebra Q :=
  Complex.lift
    ⟨CliffordAlgebra.ι Q 1, by rw [CliffordAlgebra.ι_sq_scalar, Q_apply, one_mul, RingHom.map_neg, RingHom.map_one]⟩

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