Theorem LinearMap.trace_eq_sum_trace_restrict_of_eq_biSup

Modification history

2024-02-20 23:51
Mathlib/Algebra/DirectSum/LinearMap.lean
feat: add lemma `LinearMap.trace_restrict_eq_sum_trace_restrict` (#10638)
Added LinearMap.trace_eq_sum_trace_restrict_of_eq_biSupView on Github →