Commit 2021-04-14 18:40 e4edf46d

feat(algebra/direct_sum_graded): A 0 is a ring, A i is an A 0-module, and direct_sum.of A 0 is a ring_hom (#6851) In a graded ring, grade 0 is itself a ring, and grade i (and therefore, the overall direct_sum) is a module over elements of grade 0. This stops just short of the structure necessary to make a graded ring a graded algebra over elements of grade 0; this requires some extra assumptions and probably a new typeclass, so is best left to its own PR. The main results here are direct_sum.grade_zero.comm_ring, direct_sum.grade_zero.semimodule, and direct_sum.of_zero_ring_hom. Note that we have no way to let the user provide their own ring structure on A 0, as [Π i, add_comm_monoid (A i)] [semiring (A 0)] provides add_comm_monoid (A 0) twice.