Skip to main content
To KTH's start page To KTH's start page

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

Bachelor thesis presentation

Time: Tue 2022-06-07 14.00 - 15.00

Location: Kräftriket, house 6, room 306

Respondent: Daniel Michel Nick Skantz

Export to calendar


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.