Metamath Proof Explorer


Table of Contents - 11.3.6. Cramer's rule

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).

  1. slesolvec
  2. slesolinv
  3. slesolinvbi
  4. slesolex
  5. cramerimplem1
  6. cramerimplem2
  7. cramerimplem3
  8. cramerimp
  9. cramerlem1
  10. cramerlem2
  11. cramerlem3
  12. cramer0
  13. cramer