ofComplex_comp_toComplex — Mathlib

English

There is a canonical real‑algebra isomorphism between the Clifford algebra on Q and the complex numbers.

Русский

Существует канонический тождественный как реальное алгебровое пространство изоморфизм между CliffordAlgebra(Q) и ℂ.

LaTeX

$$$\operatorname{CliffordAlgebra}(Q) \cong_{\mathbb{R}} \mathbb{C}$$$

Lean4

@[simp]
theorem ofComplex_comp_toComplex : ofComplex.comp toComplex = AlgHom.id ℝ (CliffordAlgebra Q) :=
  by
  ext
  dsimp only [LinearMap.comp_apply, Subtype.coe_mk, AlgHom.id_apply, AlgHom.toLinearMap_apply, AlgHom.comp_apply]
  rw [toComplex_ι, one_smul, ofComplex_I]

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