Commit 2021-11-03 22:10 fed57b54

refactor(algebra/direct_sum): rework internally-graded objects (#10127) This is a replacement for the graded_ring.core typeclass in #10115, which is called set_like.graded_monoid here. The advantage of this approach is that we can use the same typeclass for graded semirings, graded rings, and graded algebras. Largely, this change replaces a bunch of defs with instances, by bundling up the arguments to those defs to a new typeclass. This seems to make life easier for the few global gmonoid instance we already provide for direct sums of submodules, suggesting this API change is a useful one. In principle the new [set_like.graded_monoid A] typeclass is useless, as the same effect can be achieved with [set_like.has_graded_one A] [set_like.has_graded_mul A]; pragmatically though this is painfully verbose, and probably results in larger term sizes. We can always remove it later if it causes problems.