mathlib

5fd36643 - feat(algebra/graded_monoid): Split out graded monoids from graded rings (#9586)

feat(algebra/graded_monoid): Split out graded monoids from graded rings (#9586) This cleans up the `direct_sum.gmonoid` typeclass to not contain a bundled morphism, which allows it to be used to describe graded monoids too, via the alias for `sigma` `graded_monoid`. Essentially, this: * Renames: * `direct_sum.ghas_one` to `graded_monoid.has_one` * `direct_sum.ghas_mul` to `direct_sum.gnon_unital_non_assoc_semiring` * `direct_sum.gmonoid` to `direct_sum.gsemiring` * `direct_sum.gcomm_monoid` to `direct_sum.gcomm_semiring` * Introduces new typeclasses which represent what the previous names should have been: * `graded_monoid.ghas_mul` * `graded_monoid.gmonoid` * `graded_monoid.gcomm_monoid` This doesn't do as much deduplication as I'd like, but it at least manages some. There's not much in the way of new definitions here either, and most of the names are just copied from the graded ring case.