mathlib

140e17b8 - feat(algebra/direct_sum_graded): a direct_sum of copies of a ring is itself a ring (#7420)

feat(algebra/direct_sum_graded): a direct_sum of copies of a ring is itself a ring (#7420) Once this is in, it's straightforward to show `add_monoid_algebra R ι ≃+* ⨁ i : ι, R` Co-authored-by: Johan Commelin <johan@commelin.net>