As pointed out in the examples for the CommRingSolver, there are problems with using concrete rings, e.g. the integers.
This is due to the normalisation of the goal that currently happens before the actual parsing of the ring expressions. To fix the problem, it might be enough to just not normalise the goal and introduce matching for the binary minus ´´´-´´´.
As pointed out in the examples for the CommRingSolver, there are problems with using concrete rings, e.g. the integers. This is due to the normalisation of the goal that currently happens before the actual parsing of the ring expressions. To fix the problem, it might be enough to just not normalise the goal and introduce matching for the binary minus ´´´-´´´.