mathlib

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