mathlib3 documentation

Star structure on clifford_algebra #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

theorem clifford_algebra.star_smul {R : Type u_1} [comm_ring R] {M : Type u_2} [add_comm_group M] [module R M] {Q : quadratic_form R 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.