Mathlib Changelog
Changelog
About
Github
Def
direct_sum.decompose_linear_equiv
Modification history
2022-06-16 19:20
src/algebra/direct_sum/decomposition.lean
feat(algebra/direct_sum/decomposition): add decompositions into a direct sum (#14626) …
Added
direct_sum.decompose_linear_equiv
View on Github →