Let $k$ be a field equipped with a polynomially controlled encoding: equality with $0_k$, addition, subtraction, multiplication, and inversion of nonzero encoded field elements are computable in polynomial time, and the lengths of encodings produced by any polynomially bounded sequence of these operations are bounded by a polynomial in the input lengths.

Given positive integers $m,n$, a matrix $A \in k^{m \times n}$, and a vector $b \in k^m$, all presented by valid entrywise encodings, there is an algorithm which decides whether the linear system $Ax=b$ has a solution in $k^n$ and, if a solution exists, outputs one encoded vector $x \in k^n$ satisfying $Ax=b$. The running time is bounded by a polynomial in $m$, $n$, and the total encoding length of the entries of $A$ and $b$.