Theorem Matrix.trace_diagonal

Modification history

2025-08-11 13:25

Mathlib/LinearAlgebra/Matrix/Trace.lean

chore: split file `LinearAlgebra.RootSystem.GeckConstruction.Basic` (#28089) …

Modified Matrix.trace_diagonal View on Github →

2023-09-09 23:05

Mathlib/LinearAlgebra/Matrix/Trace.lean

feat(LinearAlgebra/Matrix/Trace): add Matrix.trace_diagonal (#7061) …

Added Matrix.trace_diagonal View on Github →