Trace of a matrix #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
Any changes to this file require a corresponding PR to mathlib4.
This file defines the trace of a matrix, the map sending a matrix to the sum of its diagonal
linear_algebra.trace for the trace of an endomorphism.
matrix, trace, diagonal
The trace of a square matrix. For more bundled versions, see: