trace_diagonal — Mathlib

English

Let d: o → R with o finite. Then the trace of the diagonal matrix diag(d) is the sum of the entries d_i: tr(diag(d)) = ∑_i d_i.

Русский

Пусть d: o → R; для диагональной матрицы diag(d) выполняется tr(diag(d)) = ∑_i d_i.

LaTeX

$$$$ \operatorname{tr}(\operatorname{diag}(d)) = \sum_i d_i $$$$

Lean4

@[simp]
theorem trace_diagonal {o} [Fintype o] [DecidableEq o] (d : o → R) : trace (diagonal d) = ∑ i, d i := by
  simp only [trace, diag_apply, diagonal_apply_eq]

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