ofComplex_conj — Mathlib

English

Complex conjugation corresponds to the involute under the canonical equivalence between ℂ and CliffordAlgebra(Q).

Русский

Комплексное сопряжение соответствует инвольюции через каноническое соответствие между ℂ и CliffordAlgebra(Q).

LaTeX

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

Lean4

/-- `Complex.conj` is analogous to `CliffordAlgebra.involute`. -/
@[simp]
theorem ofComplex_conj (c : ℂ) : ofComplex (conj c) = involute (ofComplex c) :=
  CliffordAlgebraComplex.equiv.injective <| by
    rw [equiv_apply, equiv_apply, toComplex_involute, toComplex_ofComplex, toComplex_ofComplex]

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