Linear algebra

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

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

Modules in the linear algebra namespace

module linear-algebra where

open import linear-algebra.bilinear-forms-real-vector-spaces public
open import linear-algebra.cauchy-schwarz-inequality-real-inner-product-spaces public
open import linear-algebra.complex-vector-spaces public
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.large-left-modules-large-rings 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.normed-real-vector-spaces public
open import linear-algebra.orthogonality-bilinear-forms-real-vector-spaces public
open import linear-algebra.orthogonality-real-inner-product-spaces 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.real-banach-spaces public
open import linear-algebra.real-hilbert-spaces public
open import linear-algebra.real-inner-product-spaces public
open import linear-algebra.real-inner-product-spaces-are-normed public
open import linear-algebra.real-vector-spaces 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.seminormed-real-vector-spaces public
open import linear-algebra.subsets-left-modules-rings public
open import linear-algebra.symmetric-bilinear-forms-real-vector-spaces 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
open import linear-algebra.vector-spaces public

Recent changes