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.

Estimated changes