A matrix is a linear map written down in a basis; multiplying matrices is composing maps. Elimination turns a system of equations into one you can read off. The determinant is the one number that says whether the map can be undone, and it multiplies when maps are composed.
The object. A 2×2 matrix A over Fp. Choose its four entries and read off its determinant ad − bc, its rank, whether it has an inverse, and what happens to the determinant when A is multiplied by itself. The button counts all p4 matrices and compares those with det ≠ 0 to the formula (p² − 1)(p² − p).
To know a linear map on Fn you only need to know what it does to the n unit vectors: everything else is a combination of those, and the map respects combinations. List the m coordinates of each image as a column and you have a table of numbers with n columns and m rows. Doing one map and then another is then a fixed recipe on the two tables, the product, and nothing more.
Let A be the matrix of T (columns Tej) and x = Σj xjej. By linearity Tx = Σj xjTej, whose ith coordinate is Σj tijxj. Conversely that formula defines a linear map with columns Tej. For the product: the kth column of ST is S(Tek) = S(Σj tjkej) = Σj tjk Sej, whose ith coordinate is Σj sijtjk. □
Lax pp.32–35. Lean: product_is_composition, proved by Mathlib’s Matrix.mulVec_mulVec; it checks the statement, not this proof, and the file compiles. The script checks: (AB)v = A(Bv) for every pair of 2×2 matrices over F2 (256 pairs), over F3 (6,561 pairs) and every pair of 3×3 matrices over F2 (262,144 pairs), each on every vector. Control: over F3, with A = [[1,1],[0,1]] and B = [[1,0],[1,1]], AB = [[2,1],[1,1]] and BA = [[1,1],[1,2]]; matrix multiplication is not commutative, which is why the order in the rule matters.
To solve a system, you add multiples of one equation to another until each unknown can be read off, swapping equations when a leading coefficient is zero. None of these moves changes the set of solutions, because each can be undone. What is left is a staircase, and the number of steps is the rank.
Solve Ax = b with A = [[0,2,1],[1,1,1],[2,1,3]] and b = (4, 6, 11). The first pivot is zero, so swap rows 1 and 2: rows (1,1,1 | 6), (0,2,1 | 4), (2,1,3 | 11). Subtract 2×row 1 from row 3: (0,−1,1 | −1). Halve row 2: (0,1,½ | 2). Add row 2 to row 3: (0,0,3/2 | 1). Back-substitute: x3 = 2/3, x2 = 2 − (½)(2/3) = 5/3, x1 = 6 − 5/3 − 2/3 = 11/3. Check in the original equations: 0 + 10/3 + 2/3 = 4, 11/3 + 5/3 + 2/3 = 6, 22/3 + 5/3 + 6/3 = 11. For the right-hand side (5, 6, 13) the same steps give x = (7/3, 4/3, 7/3).
A singular case: [[1,2],[2,4]] has rank 1 (the second row is twice the first). The system with right-hand side (1, 2) is consistent and has a whole line of solutions; with (1, 3) the second equation contradicts the first and there is none. The proof that row rank equals column rank is Lax’s (Theorem 6, p.27); the script checks it, below, on every matrix of the stated sizes.
Lean: rank_transpose_eq, Mathlib’s Matrix.rank_transpose. The file does not state elimination itself. The script solves the worked system in exact rational arithmetic (x = (11/3, 5/3, 2/3), one row swap) and by substitution, and checks row rank = column rank, together with |range| = prank, for every 2×3 and 3×2 matrix over F2 and F3 and every 3×3 matrix over F2 (64 + 64 + 729 + 729 + 512 matrices). This is the link to chapter 5: the range of a matrix has prank elements.
Over the reals the determinant of an n×n matrix is the factor by which the map scales volume, with a sign for whether it flips orientation. Two things follow at once: composing two maps multiplies the factors, and a map that squashes volume to zero cannot be undone. Over a finite field there is no volume, but the algebra survives: a formula for det that is linear in each column, changes sign when two columns are swapped, and is 1 on the identity.
Theorem 2, in the 2×2 case, by expansion. Let A = [[a,b],[c,d]] and B = [[e,f],[g,h]]. Then BA = [[ea + fc, eb + fd],[ga + hc, gb + hd]], and (ea + fc)(gb + hd) − (eb + fd)(ga + hc) = eahd + fcgb − ebhc − fdga (the terms eagb and ebga, and fchd and fdhc, cancel in pairs) = (ad − bc)(eh − fg). In general both sides, as functions of the columns of A, are linear in each column, change sign when two columns are swapped, and agree (to det B) at A = I; such a function is unique up to its value at I, which is Lax’s argument on p.49.
Corollary 3. If AB = I then det A det B = det I = 1, so det A ≠ 0. Conversely, if det A ≠ 0 then A(adj A) = (det A)I (Section 4), so A has the inverse (det A)−1 adj A. □
The count. A matrix is invertible exactly when its columns form a basis, and the columns can be chosen one at a time: the first is any nonzero vector (pn − 1 choices), the second any vector outside the line of the first (pn − p), the third outside the plane of the first two (pn − p2), and so on.
Lax pp.44–51. Lean: det_product, invertible_iff_det_ne_zero (Mathlib’s Matrix.det_mul and Matrix.isUnit_iff_isUnit_det), both compiled. The script checks the Leibniz formula against cofactor expansion on 200 random integer 4×4 matrices (fixed seed); det(BA) = det A det B for every pair of 2×2 matrices over F2 (256 pairs), F3 (6,561), F5 (390,625) and every pair of 3×3 over F2 (262,144); that a matrix has an inverse, found by search, exactly when det ≠ 0 (2×2 over F2 and F3, 3×3 over F2); the four counts above; and that swapping the rows of [[1,2],[3,4]] changes det from −2 to 2. Controls: det(I + I) = 4 but det I + det I = 2, so the determinant is not additive; and 3×3 over F3 has 11,232 matrices with det ≠ 0, not 39/2.
The determinant also gives a closed formula for the solution of a square system. It is a good way to see how the answer depends on the data, and a poor way to compute one: the Leibniz formula has n! terms, and elimination does the same job in far fewer steps.
For the matrix of Section 2, det A = −3 and adj(A) = [[2,−5,1],[−1,−2,1],[−1,4,−2]]; multiplying out, A adj(A) = −3I. For b = (4, 6, 11), replacing columns of A by b in turn and dividing by −3 gives x = (11/3, 5/3, 2/3), the same answer elimination gave. The proof of the rule is Lax’s (p.54): expanding det Ak along column k and using that a determinant with two equal columns is zero.
Lean: cramer_solves states A(cramer A b) = (det A)·b, from Mathlib’s Matrix.mulVec_cramer; it does not need det A ≠ 0, and it compiles. The script checks the example in exact arithmetic: Cramer’s quotients equal the elimination solution, A adj(A) = det A · I with the adjugate above, and A−1b = x. Control: [[1,2],[2,4]] has determinant 0, so the rule has nothing to divide by.
Changing the basis changes the matrix of a map to P A P−1. Quantities that mean something about the map itself, not the basis, must survive that change. The determinant does, by Theorem 2. The sum of the diagonal entries does too, because it does not care about the order of a product.
tr(AB) = Σi Σk aikbki, and swapping the names of the summation indices gives Σk Σi bkiaik = tr(BA). Then tr(P A P−1) = tr(A P−1P) = tr A, and det(P A P−1) = det P det A det P−1 = det A, because det P det P−1 = det I = 1. □
Lean: trace_comm (Matrix.trace_mul_comm) and similar_det (Matrix.det_conj), both compiled. The script checks: tr(AB) = tr(BA) for all 262,144 pairs of 3×3 matrices over F2, and, over F3, that P A P−1 has the same determinant and trace as A for all 48 invertible P and all 81 matrices A (3,888 cases). Controls: tr(AB) is not tr A · tr B (for A = B = I: 2 against 4); and the converse of Theorem 9 is false: over F3, I and [[1,1],[0,1]] have the same determinant and trace, but every conjugate of I is I itself, so the two are not similar.
Lax works over the reals or complex numbers, and his motivation for the determinant is volume. The algebra in Sections 1 to 5 uses only that the entries lie in a field (the Leibniz formula, Theorem 2 and the trace results hold over any commutative ring; the equivalence in Corollary 3 needs a field; over a general commutative ring the condition is that det A is a unit). The finite-field checks therefore say something about those statements and nothing about the volume interpretation, which needs the reals.