Commutative and non-commutative algebras

Open pi8027 opened this issue 2 years ago • 1 comments

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.

Feb 15 '23 10:02 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)

May 22 '23 21:05 pi8027