mathlib

fed57b54 - refactor(algebra/direct_sum): rework internally-graded objects (#10127)

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 `def`s 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. Co-authored-by: Jujian Zhang <jujian.zhang1998@outlook.com>