Mathlib v3 is deprecated. Go to Mathlib v4

Theorem matrix.trace_mul_comm

Modification history

2022-05-02 11:44
src/linear_algebra/matrix/trace.lean
refactor(linear_algebra/trace): unbundle `matrix.trace` (#13712) …
Modified matrix.trace_mul_commView on Github →
2021-08-08 11:51
src/linear_algebra/matrix/trace.lean
chore(linear_algebra/matrix/trace): relax `comm_ring` to `comm_semiring` in `matrix.trace_mul_comm` (#8577)
Modified matrix.trace_mul_commView 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.trace_mul_commView on Github →
2020-04-07 03:42
src/linear_algebra/matrix.lean
chore(algebra/big_operators): drop some `decidable_eq` assumptions (#2332) …
Modified matrix.trace_mul_commView on Github →
2020-01-31 17:07
src/linear_algebra/matrix.lean
feat(linear_algebra/matrix): Add proof that trace AB = trace BA, for matrices. (#1913) …
Added matrix.trace_mul_commView on Github →