trace_complex_apply — Mathlib

English

Let z ∈ ℂ be viewed as an element of an ℝ-algebra ℂ. The trace from ℂ to ℝ of z equals 2·Re(z).

Русский

Пусть z ∈ ℂ рассматривается как элемент ℂ над ℝ. След из ℂ в ℝ равен 2·Re(z).

LaTeX

$$$\\mathrm{trace}_{\\mathbb{R}}^{\\mathbb{C}}(z) = 2 \\operatorname{Re}(z)$$$

Lean4

theorem trace_complex_apply (z : ℂ) : Algebra.trace ℝ ℂ z = 2 * z.re :=
  by
  rw [Algebra.trace_eq_matrix_trace Complex.basisOneI, Algebra.leftMulMatrix_complex, Matrix.trace_fin_two]
  exact (two_mul _).symm

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