map_mul — Mathlib

English

For any two elements a and b in the Clifford algebra, reverse(a b) = reverse(b) reverse(a). This expresses that reverse reverses the order of multiplication.

Русский

Для любых элементов a и b в клиффидовой алгебре reverse(a b) = reverse(b) reverse(a). Это выражает, что reverse разворачивает порядок умножения.

LaTeX

$$$ reverse(a b) = reverse(b) \; reverse(a) $$$

Lean4

@[simp]
protected theorem map_mul (a b : CliffordAlgebra Q) : reverse (a * b) = reverse b * reverse a :=
  op_injective (map_mul reverseOp a b)

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