Theorem DirectSum.decomposeAddEquiv_apply

Modification history

2025-01-14 01:19
Mathlib/Algebra/DirectSum/Decomposition.lean
chore: address `simps` porting notes (#20717) …
Deleted DirectSum.decomposeAddEquiv_applyView on Github →
2023-05-25 11:24
Mathlib/Algebra/DirectSum/Decomposition.lean
feat: port Algebra.Module.GradedModule (#4228) …
Added DirectSum.decomposeAddEquiv_applyView on Github →