here is an algebra question for a change.
I need a version of MonoidRing for MonoidWithZero.
That is, the monoid has a "zero" element which also becomes the zero
element of its monoid ring and thus needs special treatment.
For this I need (so I think) both a Category MonoidWithZero, which is
easy, and a special version of MonoidRing which knows how to treat the zero
element. I would like to reuse as much as possible from MonoidRing,
however I realized that MonoidRingCategory is only locally defined in
mring.spad:
MonoidRing(R: Ring, M: Monoid): MRcategory == MRdefinition where
Term ==> Record(coef: R, monom: M)
MRcategory ==> Join(Ring, RetractableTo M, RetractableTo R) with
...
Is there a smart way to reuse this without completely rewriting it?