Theorem DirectSum.toAddMonoidHom_lmap

Modification history

2025-03-05 02:59
Mathlib/Algebra/DirectSum/Module.lean
feat(Algebra/DirectSum): getting a map between directsums by giving the map on components (#22354) …
Added DirectSum.toAddMonoidHom_lmapView on Github →