toComplex — Mathlib

English

The involution on CliffordAlgebra Q corresponds to complex conjugation under the toComplex map.

Русский

Инволюция в CliffordAlgebra(Q) соответствует комплексному сопряжению через отображение toComplex.

LaTeX

$$$\operatorname{toComplex}(\operatorname{involute}(c)) = \overline{\operatorname{toComplex}(c)}$$$

Lean4

/-- Intermediate result for `CliffordAlgebraComplex.equiv`: clifford algebras over
`CliffordAlgebraComplex.Q` above can be converted to `ℂ`. -/
def toComplex : CliffordAlgebra Q →ₐ[ℝ] ℂ :=
  CliffordAlgebra.lift Q
    ⟨LinearMap.toSpanSingleton _ _ Complex.I, fun r =>
      by
      dsimp [LinearMap.toSpanSingleton, LinearMap.id]
      rw [mul_mul_mul_comm]
      simp⟩

Похожие утверждения