English
The involution acts compatibly with base change on the Clifford algebra: applying toBaseChange to the involute of an element x yields the tensor product map of id on the left and involute on the right, applied to toBaseChange x.
Русский
Инволюция действует совместимо с изменением базы: применение toBaseChange к involute x равно применению тензорного произведения с iд слева и involute справа к x.
LaTeX
$$$toBaseChange(A,Q)(\mathrm{involute}(x)) = (\mathrm{Id}_A \otimes \mathrm{involute}) (toBaseChange(A,Q)(x))$$$
Lean4
/-- The involution acts only on the right of the tensor product. -/
theorem toBaseChange_involute (Q : QuadraticForm R V) (x : CliffordAlgebra (Q.baseChange A)) :
toBaseChange A Q (involute x) = TensorProduct.map LinearMap.id (involute.toLinearMap) (toBaseChange A Q x) :=
DFunLike.congr_fun (toBaseChange_comp_involute A Q) x
