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 outline of the proof for systems of linear equations with coefficients from a commutative ring, according to the proof in Wikipedia (https://en.wikipedia.org/wiki/Cramer's_rule#A_short_proof), is as follows:
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).