Theorem Matrix.trace_eq_zero_of_isEmpty

Modification history

2023-09-04 13:18
Mathlib/LinearAlgebra/Matrix/Trace.lean
feat: nilpotent matrices have nilpotent trace (#6588) …
Added Matrix.trace_eq_zero_of_isEmptyView on Github →