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

Created src/algebra/monoid_algebra_to_direct_sum.lean

added def add_monoid_algebra.to_direct_sum

added theorem add_monoid_algebra.to_direct_sum_add

added theorem add_monoid_algebra.to_direct_sum_mul

added theorem add_monoid_algebra.to_direct_sum_single

added theorem add_monoid_algebra.to_direct_sum_to_add_monoid_algebra

added theorem add_monoid_algebra.to_direct_sum_zero

added def add_monoid_algebra_equiv_direct_sum

added def direct_sum.to_add_monoid_algebra

added theorem direct_sum.to_add_monoid_algebra_add

added theorem direct_sum.to_add_monoid_algebra_mul

added theorem direct_sum.to_add_monoid_algebra_of

added theorem direct_sum.to_add_monoid_algebra_to_direct_sum

added theorem direct_sum.to_add_monoid_algebra_zero