reverse_eq_id — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem reverse_eq_id : (reverse : CliffordAlgebra (0 : QuadraticForm R Unit) →ₗ[R] _) = LinearMap.id :=
  LinearMap.ext reverse_apply

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