involute_eq_id — Mathlib

English

Let R be a commutative ring. The involute map on the Clifford algebra of the zero‑dimensional quadratic form on the unit type is the identity map.

Русский

Пусть R — коммутативное кольцо. Инволютная карта клиффордовой алгебры нулевой размерности равна тождественному отображению.

LaTeX

$$$\operatorname{involute} = \mathrm{Id}_{\operatorname{CliffordAlgebra}(0 : \operatorname{QuadraticForm} R\,\mathrm{Unit})}$$$

Lean4

@[simp]
theorem involute_eq_id : (involute : CliffordAlgebra (0 : QuadraticForm R Unit) →ₐ[R] _) = AlgHom.id R _ := by ext; simp

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