trace_toLin'_eq — Mathlib

English

The trace of A as a linear map via the canonical isomorphism equals A's trace.

Русский

След A как линейного отображения через каноническое изоморфирование равен следу A.

LaTeX

$$$\\operatorname{trace}_R (\\_, \\_) A^\\mathrm{toLin'} = A^\\mathrm{trace}$$$

Lean4

@[simp]
theorem _root_.Matrix.trace_toLin'_eq (A : Matrix ι ι R) : LinearMap.trace R _ A.toLin' = A.trace :=
  A.trace_toLin_eq (Pi.basisFun R ι)

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