Constructive quantifier elimination with a focus on matrix rings

We give a sufficient condition for a model theoretic structure B to ‘inherit’ quantifier elimination from another structure A . This yields an alternative proof of one of the main results from [8] , namely quantifier elimination for certain matrix rings. The original proof uses model theory, and while it is very elegant and insightful, the proof we propose is much shorter and provides a constructive algorithm.