reverse_involute_commute — Mathlib

English

Reverse and involute commute as functions: reverse and involute can be applied in either order and give the same result.

Русский

Reverse и involute коммутируют как функции: их можно применять в любом порядке и получить одинаковый результат.

LaTeX

$$$ \text{reverse} \circ \text{involute} = \text{involute} \circ \text{reverse} $$$

Lean4

/-- `CliffordAlgebra.reverse` and `CliffordAlgebra.involute` commute. Note that the composition
is sometimes referred to as the "clifford conjugate". -/
theorem reverse_involute_commute : Function.Commute (reverse (Q := Q)) involute :=
  LinearMap.congr_fun reverse_comp_involute

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