Commit 2021-05-05 18:50 140e17b8
View on Github →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
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