# mathlibdocumentation

linear_algebra.clifford_algebra.star

# Star structure on clifford_algebra#

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 clifford_algebra.star_def.

## Main definitions #

• clifford_algebra.star_ring
@[protected, instance]
def clifford_algebra.star_ring {R : Type u_1} [comm_ring R] {M : Type u_2} [ M] {Q : M} :
Equations
theorem clifford_algebra.star_def {R : Type u_1} [comm_ring R] {M : Type u_2} [ M] {Q : M} (x : clifford_algebra Q) :
theorem clifford_algebra.star_def' {R : Type u_1} [comm_ring R] {M : Type u_2} [ M] {Q : M} (x : clifford_algebra Q) :
@[simp]
theorem clifford_algebra.star_ι {R : Type u_1} [comm_ring R] {M : Type u_2} [ M] {Q : M} (m : M) :
@[simp]
theorem clifford_algebra.star_smul {R : Type u_1} [comm_ring R] {M : Type u_2} [ M] {Q : M} (r : R) (x : clifford_algebra Q) :

Note that this not match the star_smul implied by star_module; 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 clifford_algebra.star_algebra_map {R : Type u_1} [comm_ring R] {M : Type u_2} [ M] {Q : M} (r : R) :