Commit 2020-01-31 17:07 5ce0c0a2
View on Github →feat(linear_algebra/matrix): Add proof that trace AB = trace BA, for matrices. (#1913)
- feat(linear_algebra/matrix): trace AB = trace BA
- Remove now-redundant matrix.smul_sum In a striking coincidence, https://github.com/leanprover-community/mathlib/pull/1910 was merged almost immediately before https://github.com/leanprover-community/mathlib/pull/1883 thus rendering matrix.smul_sum redundant.
- Make arguments explicit for matrix.trace, matrix.diag
- Tidy up whitespace
- Remove now-redundant type ascriptions
- Update src/linear_algebra/matrix.lean Co-Authored-By: Johan Commelin johan@commelin.net
- Feedback from code review
- Generalize diag_transpose, trace_transpose. With apologies to the CI for triggering another build :-/
- Explicit arguments trace, diag defs but not lemmas