trace — Mathlib

English

Let A be an n×n matrix over a commutative additive monoid R. Then the trace of A is the sum of its diagonal entries: tr(A) = ∑_{i=1}^n A_{ii}.

Русский

Пусть A — матрица размера n×n над коммутативной аддитивной моноидой R. След матрицы равен сумме ее диагональных элементов: tr(A) = ∑_{i=1}^n A_{ii}.

LaTeX

$$$$ \operatorname{tr}(A) = \sum_{i=1}^{n} A_{ii} $$$$

Lean4

/-- The trace of a square matrix. For more bundled versions, see:
* `Matrix.traceAddMonoidHom`
* `Matrix.traceLinearMap`
-/
def trace (A : Matrix n n R) : R :=
  ∑ i, diag A i

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