feat(PFunctor): Add API of basic constructions

[dtumad]

PR to add various basic PFunctor definitions from PolyFun , split off from #731 to better isolate changes for review.

Main definitions are PFunctor.monomial, PFunctor.add, and PFunctor.mul, with abbreviations for common special cases of PFunctor.monomial.

Discussion about the addition notation:
https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Universe.20unification.20with.20.60HAdd.2EhAdd.60.20vs.2E.20.60.2B.60.20notation/with/617534952.01

[eric-wieser]

It would be great to raise this issue on Zulip and link the post from the PR description.

[eric-wieser]

It would be great to have another PFunctor expert review this for docstrings, but this all looks pretty reasonable to me.

[dtumad]

Also cc @quangvdao would be good to get your review too.

Also more generally I'm unsure about adding X as notation in the first place, and also if we should add A X^ B notation for PFunctor.monomial A B from PolyFun, or just keep the explicit spelling in cslib? It does make the equations look more intuitive I think.

[dtumad]

Also cc @quangvdao would be good to get your review too.

Also more generally I'm unsure about adding X as notation in the first place, and also if we should add A X^ B notation for PFunctor.monomial A B from PolyFun, or just keep the explicit spelling in cslib? It does make the equations look more intuitive I think.

To expand on this, I think PolyFun may want to just adopt the notation from https://arxiv.org/abs/2312.00990, in which case X should maybe just be defined here as y. I sort of like the Yoneda framing with y but maybe both should exist, or neither for now. With that switch it would be A y^ B then instead.