equiv — Mathlib

English

The Clifford algebra on Q is isomorphic to ℂ as an ℝ‑algebra.

Русский

Клиффордова алгебра над Q изоморфна ℂ как ℝ‑алгебра.

LaTeX

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

Lean4

/-- The clifford algebras over `CliffordAlgebraComplex.Q` is isomorphic as an `ℝ`-algebra to `ℂ`. -/
@[simps!]
protected def equiv : CliffordAlgebra Q ≃ₐ[ℝ] ℂ :=
  AlgEquiv.ofAlgHom toComplex ofComplex toComplex_comp_ofComplex ofComplex_comp_toComplex

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