traceLinearMap — Mathlib

English

The trace is a linear map from matrices to the base ring: it is additive and homogeneous.

Русский

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

LaTeX

$$$$ \operatorname{tr}(A + B) = \operatorname{tr}(A) + \operatorname{tr}(B), \quad \operatorname{tr}(rA) = r \operatorname{tr}(A). $$$$

Lean4

/-- `Matrix.trace` as a `LinearMap` -/
@[simps]
def traceLinearMap [Semiring α] [Module α R] : Matrix n n R →ₗ[α] R
    where
  toFun := trace
  map_add' := trace_add
  map_smul' := trace_smul

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