definition. Clifford conjugate [wieser2022formalizing] [ca-000K]

✍️source

CliffordAlgebra.reverse

L∃∀N

Clifford conjugate is an algebra homomorphism \({*} : \mathcal {C}\kern -2pt\ell (Q) \to _{a} \mathcal {C}\kern -2pt\ell (Q)\), denoted \(x^{*}\) (or even \(x^\dagger \), \(x^v\) in some literatures), defined to be: \[ x^{*} = \operatorname {reverse}(\operatorname {involute}(x)) = \tau (\alpha (x)) \] for all \(x \in \mathcal {C}\kern -2pt\ell (Q)\), satisfying (as a \(*\)-ring):

1. \((x + y)^{*} = (x)^{*} + (y)^{*}\)
2. \((x y)^{*} = (y)^{*} (x)^{*}\)
3. \({*} \circ {*} = \operatorname {id}\)
4. \(1^{*} = 1\)

Note: In our current formalization in \(\textsf {Mathlib}\), the application of the involution on \(r\) is ignored, as there appears to be nothing in the literature that advocates doing this.

Clifford conjugate is denoted \(\bar {m}\) in [lounesto2001clifford] and most literatures, \(m^\ddagger \) in [chisolm2012geometric].