Commit 2020-01-26 21:08 497e692b
View on Github →feat(linear_algebra/matrix): define the trace of a square matrix (#1883)
- feat(linear_algebra/matrix): define the trace of a square matrix
- Move ring carrier to correct universe
- Add lemma trace_one, and define diag as linear map
- Define diag and trace solely as linear functions
- Diag and trace for module-valued matrices
- Fix cyclic import
- Rename matrix.mul_sum' --> matrix.smul_sum Co-Authored-By: Johan Commelin johan@commelin.net
- Trigger CI