trace_toLin_eq — Mathlib

English

For any A, f, the trace of the linear map corresponding to A via a basis equals A's trace.

Русский

Для любой матрицы A след линейного отображения, соответствующего A через базис, равен следу A.

LaTeX

$$$\\operatorname{trace}_R M ( \\mathrm{Matrix.toLin}_{b b} A ) = A_{trace}$$$

Lean4

@[simp]
theorem _root_.Matrix.trace_toLin_eq (A : Matrix ι ι R) (b : Basis ι R M) :
    LinearMap.trace R _ (Matrix.toLin b b A) = A.trace := by simp [trace_eq_matrix_trace R b]

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