Daniel Michel Nick Skantz: Formalizing Linear Algebra in UniMath – Gaussian Elimination, Matrix Foundations & Applications

Abstract:

We formalize fundamental linear algebra in UniMath, a minimal foundation for mathematics programmed in Coq. We develop the necessary background theory, including showing properties of sums over vectors, inverses, transposes and elementary row operations over matrices in order to construct and prove correctness of procedures for Gaussian elimination, including applications for solving systems of linear equations and constructing inverses of matrices. The formalization is done partly over semirings, with properties requiring additive identity, commutativity of multiplication or decidable equality being formalized over fields.