Mathlib Changelog
v4
Changelog
About
Github
Theorem
DirectSum.isInternal_biSup_submodule_of_independent
Modification history
2024-02-20 23:51
Mathlib/Algebra/DirectSum/Module.lean
feat: add lemma `LinearMap.trace_restrict_eq_sum_trace_restrict` (#10638)
Added
DirectSum.isInternal_biSup_submodule_of_independent
View on Github →