instStarRing — Mathlib

English

In Clifford algebras, the star operation is defined as the reverse of the involution: star x = reverse (involute x).

Русский

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

LaTeX

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

Lean4

instance instStarRing : StarRing (CliffordAlgebra Q)
    where
  star x := reverse (involute x)
  star_involutive x := by simp only [reverse_involute_commute.eq, reverse_reverse, involute_involute]
  star_mul x y := by simp only [map_mul, reverse.map_mul]
  star_add x y := by simp only [map_add]

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