Adapt mxpoly.v to semimodules, semialgebras, and semilinear functions

[pi8027]

Motivation for this change

This PR generalizes some results in matrix.v and mxpoly.v to the "semi" case using #1125.

Dependencies

• #1125
• #1395
• #1398

Minimal TODO list

• [ ] added changelog entries with doc/changelog/make-entry.sh

• [ ] added corresponding documentation in the headers
• [ ] tried to abide by the contribution guide
• [ ] this PR contains an optimum number of meaningful commits

See this Checklist for details.

Automatic note to reviewers

Read this Checklist.

[pi8027]

Generalizing the results in qpoly.v seems to require generalizing vector.v to semi-vector spaces, which looks non-trivial (mostly because of technical issues like compatibility). I will try it later.

[pi8027]

I will cut this PR into smaller pieces. The poly.v part might already be ready. I should redo the matrix.v part (almost from scratch) based on #1385.