Linear algebra
Content created by Egbert Rijke, Louis Wasserman, Fredrik Bakke, Jonathan Prieto-Cubides, malarbol, Šimon Brandner, Fernando Chu and Garrett Figueroa.
Created on 2022-03-12.
Last modified on 2025-09-12.
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.dependent-products-left-modules-commutative-rings public open import linear-algebra.dependent-products-left-modules-rings public open import linear-algebra.diagonal-matrices-on-rings public open import linear-algebra.finite-sequences-in-abelian-groups public open import linear-algebra.finite-sequences-in-commutative-monoids public open import linear-algebra.finite-sequences-in-commutative-rings public open import linear-algebra.finite-sequences-in-commutative-semigroups 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-groups public open import linear-algebra.finite-sequences-in-monoids public open import linear-algebra.finite-sequences-in-rings public open import linear-algebra.finite-sequences-in-semigroups public open import linear-algebra.finite-sequences-in-semirings public open import linear-algebra.functoriality-matrices public open import linear-algebra.left-modules-commutative-rings public open import linear-algebra.left-modules-rings public open import linear-algebra.left-submodules-rings public open import linear-algebra.linear-combinations-tuples-of-vectors-left-modules-rings public open import linear-algebra.linear-maps-left-modules-rings public open import linear-algebra.linear-spans-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.preimages-of-left-module-structures-along-homomorphisms-of-rings public open import linear-algebra.rational-modules 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.subsets-left-modules-rings public open import linear-algebra.transposition-matrices public open import linear-algebra.tuples-on-commutative-monoids 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-monoids public open import linear-algebra.tuples-on-rings public open import linear-algebra.tuples-on-semirings public
Recent changes
- 2025-09-12. Šimon Brandner. Add linear combinations, linear spans and tuple concatenation (#1537).
- 2025-09-09. Louis Wasserman. Left modules over commutative rings (#1539).
- 2025-09-02. Louis Wasserman. Finite sums in groups and abelian groups (#1527).
- 2025-09-01. Šimon Brandner. Add submodules of left modules over rings (#1511).
- 2025-08-31. Louis Wasserman. Commutative semigroups (#1494).