Commit 2023-10-19 14:38 fca1e12a
View on Github →feat(Algebra/DirectSum/Decomposition): extensionality lemma for maps from a decomposition (#7662)
Two linear maps from a module with a decomposition agree if they agree on every piece.
Also replaces some bad simps lemmas with manual ones.