Linear algebra

Content created by Egbert Rijke, Fredrik Bakke, Louis Wasserman, Jonathan Prieto-Cubides, malarbol, Fernando Chu and Garrett Figueroa.

Created on 2022-03-12.
Last modified on 2025-08-11.

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-rings public
open import linear-algebra.diagonal-matrices-on-rings 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-semirings public
open import linear-algebra.finite-sequences-in-euclidean-domains 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-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.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.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