star_algebraMap — Mathlib

English

The star operation on Clifford algebras agrees with reverse of involute: star x = reverse (involute x).

Русский

Операция star на клиффордовой алгебре согласуется с обратной инволюцией: star x = reverse (involute x).

LaTeX

$$star x = reverse (involute x).$$

Lean4

@[simp]
theorem star_algebraMap (r : R) : star (algebraMap R (CliffordAlgebra Q) r) = algebraMap R (CliffordAlgebra Q) r := by
  rw [star_def, involute.commutes, reverse.commutes]

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