involute_involutive — Mathlib

English

The involute operation is involutive on all elements: involute(involute(a)) = a for all a in CliffordAlgebra Q.

Русский

Операция инволюции является инволютивной: involute(involute(a)) = a для всех a в CliffordAlgebra Q.

LaTeX

$$$ \forall a:\; \mathrm{CliffordAlgebra}(Q):\; \mathrm{involute}(\mathrm{involute}(a)) = a. $$$

Lean4

theorem involute_involutive : Function.Involutive (involute : _ → CliffordAlgebra Q) :=
  AlgHom.congr_fun involute_comp_involute

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