# Def direct_sum

#### Modification history

2020-10-29 18:26

src/algebra/direct_sum.lean

feat(algebra/direct_sum*): relax a lot of constraints to add_comm_monoid (#3537)

Modified direct_sumView on Github →Mathlib v3 is deprecated. Go to Mathlib v4

2020-10-29 18:26

src/algebra/direct_sum.lean

feat(algebra/direct_sum*): relax a lot of constraints to add_comm_monoid (#3537)

Modified direct_sumView on Github →