MATHLIBANNEX / CANONICAL DECLARATION CARD

Cramer’s rule for coordinates of a row

MathlibAnnex.Matrix.det_smul_vecMul_nonsingInv_eq_updateRowDet

theorem

Expresses a row in the basis of the rows of an invertible square matrix through row-replacement determinants.

Statement

Let be an -by- matrix over a field, with , and let be a row of length . If denotes replacement of row by , then

Assumptions

The scalar system is an arbitrary field, , and is any row. Nonvanishing of is the exact condition ensuring that the matrix inverse is an inverse.

Conclusion

The coordinate row satisfies , and each coordinate is . If , the equality is between the two empty coordinate families.

The row convention is essential: the unknown coordinates multiply on the left. The source obtains this formula by applying the column form of Cramer’s rule to the transpose; replacing a column of the transpose replaces the corresponding row before transposition.

Proof route

Apply Cramer’s rule to the transpose, then identify each transposed replacement determinant.

Proof steps

  1. Write . Since , the inverse exists and

    Apply the column form of Cramer’s rule to the system on the right. Its coefficient matrix satisfies , so it gives

  2. The replaced-column matrix is exactly the transpose of the replaced-row matrix:

    Dividing by gives the stated coordinate formula. For there is no coordinate to check.

Main citations

Lean source signature (exact)

theorem det_smul_vecMul_nonsingInv_eq_updateRowDet
    {n : ℕ} {K : Type v} [Field K]
    (A : _root_.Matrix (Fin n) (Fin n) K) (r : Fin n → K)
    (hA : A.det ≠ 0) :
    A.det • (r ᵥ* A⁻¹) = fun j => (A.updateRow j r).det
In the source Mathematical meaning
{n : ℕ} {K : Type v} [Field K] An arbitrary field and an integer .
(A : root.Matrix (Fin n) (Fin n) K) (r : Fin n → K) The square matrix and row vector of length .
(hA : A.det ≠ 0) The hypothesis , ensuring that is its ordinary matrix inverse.
r ᵥ* A⁻¹ The row vector , rather than matrix times a column.
In the source Mathematical meaning
fun j => (A.updateRow j r).det The coordinate family ; row is replaced and the other rows remain.
A.det • (r ᵥ* A⁻¹) = fun j => (A.updateRow j r).det For every row position , . For both coordinate families are empty.
Exact surrounding binder context (separate excerpt) 
noncomputable section

open scoped Matrix

namespace MathlibAnnex
namespace Matrix

universe u v

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project

Exact content identity

Declaration: MathlibAnnex.Matrix.det_smul_vecMul_nonsingInv_eq_updateRowDet

Accepted content SHA-256: 5659e9ecb00331a1bc04662532630b0fe758fa8181059313bc07568e406a91dd

Accepted source guide SHA-256: 095d5a0faa50d2de6a7f4eb7f83600df7d366888ba9f8f6f290e4a22f7351bb3

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑