David M. Russinoff
david@russinoff.com
http://www.russinoff.com

This directory contains an ACL2 formalization of elementary linear algebra, a work in progress.  The books of the top-level directory are listed below.  Once completed, the content will approximate that of a rigorous introductory undergraduate course in the subject.

This work is documented in two papers that appear in the 2025 ACL2 Workshop.  As explained in the first of these papers, we separate those aspects of the theory that apply to matrices over an arbitrary commutative ring with unity from those that are restricted to matrices over a field (i.e., that depend on the existence of a multiplicative inverse).  The first three books address matrices over a ring:

* ring
    - Encapsulation of the axioms for a commutative ring with unity
    - Properties of lists of ring elemants

  * rmat
    - Matrices over a ring
    - Transpose of a matrix
    - Matrix algebra: matrix addition, scalar multiplication, and matrix multiplication

  * rdet
    - Determinant of a square matrix over a ring
    - Uniqueness of the determinant as an alternating n-linear function
    - Multiplicativity of the determinant
    - Cofactor expansion and the classical adjoint

An arbitrary field is defined by a separate encapsulation.  The only difference between this and the first, aside from function names, is an additional function and a pair of associated axioms guaranteeing the existence of multiplicative inverses.  Two other books simply contain repetitions of the above results based on these functions, i.e., in the context of matrices over an arbitrary field.  In principle, these could all be derived from the above results by functional instantiation, but it was found to be more expedient just to repeat the proofs:
  
  * field

  * fmat

  * fdet

The next book, which depends on the last 3, deals with topics that apply only to matrices over a field:

  * reduction
    - Reduced row-echelon form
    - Conversion to reduced row-echelon form
    - Row reduction as matrix multiplication
    - Invertibility
    - Systems of linear equations and Cramer's rule

In the book "rational", which is incompatible with the other books, we replace the constrained functions in field.lisp with the corresponding rational functions and in this context, we reproduce the function definitions in field.lisp, fmat.lisp, fdet.lisp, and reduction.lisp.  The result is that these definitions are now executable and may be used for the purposes of testing and illustration.

Several additional books are planned.  The first 2 are based on the theory of matrices oever a field:

  * vector spaces

  * linear transformations

Finally, we shall address the topic of eigenvalues and the characteristic polynomial.  This will involve the theory of matrices over a field as well as that of matrices over a ring, applied to the ring of polynomials over a field:

  * ring of polynomials over a field

  * eigenvalues and the characteristic polynomial
