# Def direct_sum.to_group

#### 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)

Deleted direct_sum.to_groupView on Github →2020-10-23 22:12

src/algebra/direct_sum.lean

feat(algebra/direct_sum): Bundle the homomorphisms (#4754)

Modified direct_sum.to_groupView on Github →