Def matrix.trace
Modification history
2022-05-02 11:44
src/linear_algebra/matrix/trace.lean
refactor(linear_algebra/trace): unbundle `matrix.trace` (#13712) …
Modified matrix.traceView on Github →2021-08-26 13:06
src/linear_algebra/matrix/trace.lean
feat(*): remove the `fintype` requirement from matrices. (#8810) …
Modified matrix.traceView on Github →2021-05-15 14:21
src/linear_algebra/matrix.lean
refactor(linear_algebra/matrix): split matrix.lean into multiple files (#7593) …
Modified matrix.traceView on Github →2020-07-19 04:53
src/linear_algebra/matrix.lean
feat (linear_algebra/matrix): make diag and trace compatible with semirings (#3433) …
Modified matrix.traceView on Github →