Mathlib v3 is deprecated. Go to Mathlib v4

Def direct_sum.to_add_monoid

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)
Added direct_sum.to_add_monoidView on Github →