mathlib

5d873a65 - feat(algebra/monoid_algebra): add add_monoid_algebra_ring_equiv_direct_sum (#7422)

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`.