trace_eq_matrix_trace — Mathlib

English

For any endomorphism f, the trace equals the matrix trace of its matrix in any basis: trace_R M f = tr( toMatrix_b b f ).

Русский

Для любого конечного базиса след равен следу матрицы этого отображения: trace_R M f = tr( toMatrix_b b f ).

LaTeX

$$$\\operatorname{trace}_R M f = \\mathrm{tr}( \\mathrm{toMatrix}_b^b f )$$$

Lean4

theorem trace_eq_matrix_trace (f : M →ₗ[R] M) : trace R M f = Matrix.trace (LinearMap.toMatrix b b f) := by
  classical
    rw [trace_eq_matrix_trace_of_finset R b.reindexFinsetRange, ← traceAux_def, ← traceAux_def,
    traceAux_eq R b b.reindexFinsetRange]

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