reverse_involutive — Mathlib

English

The reverse map is an involution on the Clifford algebra: applying it twice gives the identity, i.e., reverse(reverse(a)) = a for all a.

Русский

Обратное отображение является инволютивом: приложение два раза даёт тождественное отображение, то есть reverse(reverse(a)) = a для всех a.

LaTeX

$$$ reverse( reverse(a) ) = a $$$

Lean4

@[simp]
theorem reverse_involutive : Function.Involutive (reverse (Q := Q)) :=
  AlgHom.congr_fun reverseOpEquiv.symm_comp

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