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 →