instCommRingCliffordAlgebraRealQ — Mathlib

English

The Clifford algebra is commutative since it is isomorphic to the complex numbers.

Русский

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

LaTeX

$$$\operatorname{CliffordAlgebra}(Q) \text{ is a commutative ring; }\, \operatorname{mul\,comm}$ holds.$$

Lean4

/-- The clifford algebra is commutative since it is isomorphic to the complex numbers.

TODO: prove this is true for all `CliffordAlgebra`s over a 1-dimensional vector space. -/
instance : CommRing (CliffordAlgebra Q) where
  mul_comm := fun x y => CliffordAlgebraComplex.equiv.injective <| by rw [map_mul, mul_comm, map_mul]

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