Mathlib Map

Map · 15

linear algebra

MSC 15 · Linear and multilinear algebra; matrix theory

10,062 declarations (8,418 theorems, 1,644 definitions) across 277 files. 7 of the 18 famous theorems listed for this area are in Mathlib (39%). 48 open conjectures here are stated in Lean.

Files are assigned to areas by a language model reading each file's documentation. Report a file that is in the wrong area.

Subareas2

  • 15A Basic linear algebra 10,011
  • 15B Special matrices 51

Famous theorems7 of 18

From the 1000+ theorems project, which classifies each theorem by MSC area.

Not yet in Mathlib · 11

In Mathlib · 7

From the 100 theorems list2

Open conjectures stated in Lean48

Statements without proofs, collected by the Formal Conjectures project.

Undergraduate topics still missing17 of 99

From Mathlib's own undergraduate checklist.

Linear algebra · 10 of 60

  • Finite-dimensional vector spaces › rank of a system of linear equations
  • Matrices › elementary row operations
  • Matrices › elementary column operations
  • Matrices › row-reduced matrices
  • Structure theory of endomorphisms › diagonalization
  • Structure theory of endomorphisms › triangularization
  • Structure theory of endomorphisms › kernels lemma
  • Structure theory of endomorphisms › Jordan normal form
  • Linear representations › examples
  • Exponential › endomorphism exponential

Bilinear and Quadratic Forms Over a Vector Space · 7 of 39

  • Bilinear forms › rank of a bilinear form
  • Endomorphisms › diagonalization of normal endomorphisms
  • Endomorphisms › simultaneous diagonalization of two real quadratic forms, with one positive-definite
  • Endomorphisms › polar decompositions in $\mathrm{GL}(n, \R)$
  • Endomorphisms › polar decompositions in $\mathrm{GL}(n, \C)$
  • Low dimensions › classification of elements of $\mathrm{O}(2, \R)$
  • Low dimensions › classification of elements of $\mathrm{O}(3, \R)$

Structures defined here7

Typeclasses defined in this area's files, most assumed first.

Files277

Largest first. The code after each file is its assigned subarea.