Theorem DirectSum.decomposeAddEquiv_apply

Modification history

2023-05-25 11:24
Mathlib/Algebra/DirectSum/Decomposition.lean
feat: port Algebra.Module.GradedModule (#4228) …
Added DirectSum.decomposeAddEquiv_applyView on Github →