Mathlib Changelog
v4
Changelog
About
Github
Def
DirectSum.map
Modification history
2025-03-14 12:06
Mathlib/Algebra/DirectSum/Basic.lean
chore: tidy various files (#22894)
Modified
DirectSum.map
View on Github →
2025-03-05 02:59
Mathlib/Algebra/DirectSum/Basic.lean
feat(Algebra/DirectSum): getting a map between directsums by giving the map on components (#22354) …
Added
DirectSum.map
View on Github →