traceAux — Mathlib

English

The trace of an endomorphism with respect to a basis is defined as the trace of its matrix in that basis.

Русский

След конечного линейного отображения относительно базиса определяется как след его матрицы в этом базисе.

LaTeX

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

Lean4

/-- The trace of an endomorphism given a basis. -/
def traceAux : (M →ₗ[R] M) →ₗ[R] R :=
  Matrix.traceLinearMap ι R R ∘ₗ
    ↑(LinearMap.toMatrix b b)
        -- Can't be `simp` because it would cause a loop.

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