Commit 2021-10-08 14:22 5fd36643

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.