mathlib
87e9becc - chore(linear_algebra/matrix/trace): relax `comm_ring` to `comm_semiring` in `matrix.trace_mul_comm` (#8577)

Commit
4 years ago
chore(linear_algebra/matrix/trace): relax `comm_ring` to `comm_semiring` in `matrix.trace_mul_comm` (#8577)
Author
Parents
Loading