Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2507.19007 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911077349982208 |
|---|---|
| author | Russinoff, David |
| author_facet | Russinoff, David |
| contents | This is the second installment of an exposition of an ACL2 formalization of elementary linear algebra. It extends the results of Part I, which covers the algebra of matrices over a commutative ring, but focuses on aspects of the theory that apply only to matrices over a field: elementary row reduction and its application to the computation of matrix inverses and the solution of simultaneous systems of linear equations.
|
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2507_19007 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | A Formalization of Elementary Linear Algebra: Part II Russinoff, David Discrete Mathematics This is the second installment of an exposition of an ACL2 formalization of elementary linear algebra. It extends the results of Part I, which covers the algebra of matrices over a commutative ring, but focuses on aspects of the theory that apply only to matrices over a field: elementary row reduction and its application to the computation of matrix inverses and the solution of simultaneous systems of linear equations. |
| title | A Formalization of Elementary Linear Algebra: Part II |
| topic | Discrete Mathematics |
| url | https://arxiv.org/abs/2507.19007 |