Linear algebra
Content created by Egbert Rijke, Fredrik Bakke, Jonathan Prieto-Cubides, Louis Wasserman, Fernando Chu and malarbol.
Created on 2022-03-12.
Last modified on 2025-05-18.
Modules in the linear algebra namespace
module linear-algebra where open import linear-algebra.constant-matrices public open import linear-algebra.constant-tuples public open import linear-algebra.diagonal-matrices-on-rings public open import linear-algebra.finite-sequences-in-commutative-rings public open import linear-algebra.finite-sequences-in-commutative-semirings public open import linear-algebra.finite-sequences-in-euclidean-domains public open import linear-algebra.finite-sequences-in-rings public open import linear-algebra.finite-sequences-in-semirings public open import linear-algebra.functoriality-matrices public open import linear-algebra.left-modules-rings public open import linear-algebra.linear-maps-left-modules-rings public open import linear-algebra.matrices public open import linear-algebra.matrices-on-rings public open import linear-algebra.multiplication-matrices public open import linear-algebra.right-modules-rings public open import linear-algebra.scalar-multiplication-matrices public open import linear-algebra.scalar-multiplication-tuples public open import linear-algebra.scalar-multiplication-tuples-on-rings public open import linear-algebra.transposition-matrices public open import linear-algebra.tuples-on-commutative-rings public open import linear-algebra.tuples-on-commutative-semirings public open import linear-algebra.tuples-on-euclidean-domains public open import linear-algebra.tuples-on-rings public open import linear-algebra.tuples-on-semirings public
Recent changes
- 2025-05-18. Louis Wasserman and malarbol. Linear maps over modules (#1395).
- 2025-05-14. Louis Wasserman. Refactor linear algebra to use “tuples” for what was “vectors” (#1397).
- 2024-09-23. Fredrik Bakke. Some typos, wording improvements, and brief prose additions (#1186).
- 2023-05-06. Egbert Rijke. Collecting some easily defined precategories (#598).
- 2023-04-05. Fernando Chu. Euclidean domains (#547).