English
The Clifford algebra over the zero‑dimensional quadratic form on R‑modules is canonically isomorphic to R itself as an algebra.
Русский
Клиффордова алгебра нулевой размерности над R изоморфна R как R‑алгебра.
LaTeX
$$$\operatorname{CliffordAlgebra}(0 : \operatorname{QuadraticForm} R\,\mathrm{Unit}) \cong_R R$$$
Lean4
/-- The clifford algebra over a 0-dimensional vector space is isomorphic to its scalars. -/
protected def equiv : CliffordAlgebra (0 : QuadraticForm R Unit) ≃ₐ[R] R :=
AlgEquiv.ofAlgHom
(CliffordAlgebra.lift (0 : QuadraticForm R Unit) <|
⟨0, fun _ : Unit => (zero_mul (0 : R)).trans (algebraMap R _).map_zero.symm⟩)
(Algebra.ofId R _) (by ext) (by ext : 1; rw [ι_eq_zero, LinearMap.comp_zero, LinearMap.comp_zero])
