Commutative and non-commutative algebras

[pi8027]

It would be nice to support commutative and non-commutative algebras in general. The interesting part would be that scalars are still commutative in non-commutative algebras and thus requires a new reflexive decision procedure. Is it also possible to solve matrix equations by erasing the size information, e.g., embedding matrices to infinitely large matrices represented as finmap?

This feature would automatically solve #64.

[pi8027]

Is it also possible to solve matrix equations by erasing the size information, e.g., embedding matrices to infinitely large matrices represented as finmap?

A potential answer: https://doi.org/10.2168/LMCS-8(2:13)2012 (see Section 2.4)