mathlib

5ce0c0a2 - feat(linear_algebra/matrix): Add proof that trace AB = trace BA, for matrices. (#1913)

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 Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>