English
The complex‑conjugation intertwines with involution under the toComplex map; more precisely, toComplex ∘ involute equals conj ∘ toComplex.
Русский
Через отображение toComplex сопряжение комплексное сочетается с инвольюцией: toComplex ∘ involute = conj ∘ toComplex.
LaTeX
$$$\operatorname{toComplex} \circ \operatorname{involute} = \operatorname{conj} \circ \operatorname{toComplex}$$$
Lean4
/-- `CliffordAlgebra.involute` is analogous to `Complex.conj`. -/
@[simp]
theorem toComplex_involute (c : CliffordAlgebra Q) : toComplex (involute c) = conj (toComplex c) :=
by
have : toComplex (involute (ι Q 1)) = conj (toComplex (ι Q 1)) := by
simp only [involute_ι, toComplex_ι, map_neg, one_smul, Complex.conj_I]
suffices toComplex.comp involute = Complex.conjAe.toAlgHom.comp toComplex by exact AlgHom.congr_fun this c
ext : 2
exact this
