# Star structure on CliffordAlgebra#

This file defines the "clifford conjugation", equal to reverse (involute x), and assigns it the star notation.

This choice is somewhat non-canonical; a star structure is also possible under reverse alone. However, defining it gives us access to constructions like unitary.

Most results about star can be obtained by unfolding it via CliffordAlgebra.star_def.

## Main definitions #

• CliffordAlgebra.instStarRing
instance CliffordAlgebra.instStarRing {R : Type u_1} [] {M : Type u_2} [] [Module R M] {Q : } :
Equations
• CliffordAlgebra.instStarRing =
theorem CliffordAlgebra.star_def {R : Type u_1} [] {M : Type u_2} [] [Module R M] {Q : } (x : ) :
star x = CliffordAlgebra.reverse (CliffordAlgebra.involute x)
theorem CliffordAlgebra.star_def' {R : Type u_1} [] {M : Type u_2} [] [Module R M] {Q : } (x : ) :
star x = CliffordAlgebra.involute (CliffordAlgebra.reverse x)
@[simp]
theorem CliffordAlgebra.star_ι {R : Type u_1} [] {M : Type u_2} [] [Module R M] {Q : } (m : M) :
star ( m) = - m
@[simp]
theorem CliffordAlgebra.star_smul {R : Type u_1} [] {M : Type u_2} [] [Module R M] {Q : } (r : R) (x : ) :
star (r x) = r star x

Note that this not match the star_smul implied by StarModule; it certainly could if we also conjugated all the scalars, but there appears to be nothing in the literature that advocates doing this.

@[simp]
theorem CliffordAlgebra.star_algebraMap {R : Type u_1} [] {M : Type u_2} [] [Module R M] {Q : } (r : R) :
star (() r) = () r