In the following, Cramer's rule cramer is proven. According to Wikipedia
"Cramer's rule", 21-Feb-2019,
https://en.wikipedia.org/wiki/Cramer%27s_rule:
"[Cramer's rule] ... expresses the [unique] solution [of a system of linear
equations] in terms of the determinants of the (square) coefficient matrix
and of matrices obtained from it by replacing one column by the column vector
of right-hand sides of the equations."

The system of linear equations to be solved shall be given by
the N x N coefficient matrix and the N-dimensional vector .
Let be the matrix obtained by replacing the i-th column of the
coefficient matrix by the right-hand side vector . Additionally,
let be the matrix obtained by replacing the i-th column of the
identity matrix by the solution vector , with .
Finally, it is assumed that det is a unit in the underlying ring.

With these definitions, it follows that
(cramerimplem2), using matrix multiplication (mamuval) and
multiplication of a vector with a matrix (mulmarep1gsum2). By using the
multiplicativity of the determinant (mdetmul) it follows that
det det det det
(cramerimplem3).

Furthermore, it follows that det
(cramerimplem1). To show this, a special case of the Laplace expansion is
used (smadiadetg).

From these equations and the cancellation law for division in a ring
(dvrcan3) it follows that det
det det .

This is the right to left implication (cramerimp, cramerlem1,
cramerlem2) of Cramer's rule (cramer). The left to right implication
is shown by cramerlem3, using the fact that a solution of the system of
linear equations exists (slesolex).

Notice that for the special case of 0-dimensional matrices/vectors only the
left to right implication is valid (see cramer0), because assuming the
right-hand side of the implication (), could be
anything (see mavmul0g).