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]