Mathlib v3 is deprecated. Go to Mathlib v4

Theorem linear_map.trace_eq_matrix_trace_of_finite_set

Modification history

2021-06-12 08:06
src/linear_algebra/trace.lean
feat(linear_algebra): use `finset`s to define `det` and `trace` (#7778) …
Deleted linear_map.trace_eq_matrix_trace_of_finite_setView on Github →
2021-05-15 14:21
src/linear_algebra/matrix.lean
refactor(linear_algebra/matrix): split matrix.lean into multiple files (#7593) …
Modified linear_map.trace_eq_matrix_trace_of_finite_setView on Github →
2021-05-10 07:36
src/linear_algebra/matrix.lean
refactor(*): bundle `is_basis` (#7496) …
Added linear_map.trace_eq_matrix_trace_of_finite_setView on Github →