CliffordAlgebra.coe_toEven_reverse_involute

theorem CliffordAlgebra.coe_toEven_reverse_involute : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (Q : QuadraticForm R M) (x : CliffordAlgebra Q), ↑((CliffordAlgebra.toEven Q) (CliffordAlgebra.reverse (CliffordAlgebra.involute x))) = CliffordAlgebra.reverse ↑((CliffordAlgebra.toEven Q) x)

This theorem states that for any commutative ring `R`, additive commutative group `M`, and `M` being an `R`-module, given a quadratic form `Q` on `M`, and an element `x` of the Clifford algebra of `Q`, the representation of the Clifford conjugate (which is the composition of grade reversion and grade involution) in the even subalgebra of the Clifford algebra is the same as the reverse of the representation of `x` in the even subalgebra. In other words, the map which sends `x` to its Clifford conjugate commutes with the embedding from the Clifford algebra into its even subalgebra.

More concisely: For any commutative ring `R`, additive commutative group `M` making `M` an `R`-module, and quadratic form `Q` on `M`, the map from `x` in the Clifford algebra of `Q` to its Clifford conjugate in the even subalgebra equals the reverse of `x` in the even subalgebra.