# Commit 2021-05-07 09:30 5d873a65

View on Github →feat(algebra/monoid_algebra): add add_monoid_algebra_ring_equiv_direct_sum (#7422)
The only interesting result here is:
add_monoid_algebra_ring_equiv_direct_sum : add_monoid_algebra M ι ≃+* ⨁ i : ι, M
The rest of the new file is just boilerplate to translate `dfinsupp.single`

into `direct_sum.of`

.