This gives pointers to undergraduate maths topics that are currently covered in mathlib. There is also a page listing undergraduate maths topics that are not yet in mathlib.

#### Linear algebra

Finite-dimensional vector spaces finite-dimensionality, isomorphism with $K^n$, rank of a linear map, isomorphism with bidual.

Multilinearity multilinear map, determinant of vectors.

Endomorphism polynomials minimal polynomial, characteristic polynomial, Cayley-Hamilton theorem.

Structure theory of endomorphisms eigenvalue, eigenvector, generalized eigenspaces.

#### Group Theory

Permutation group permutation group of a type, signature.

Classical automorphism groups general linear group, special linear group.

#### Ring Theory

Fundamentals ring, subrings, ring morphisms, ring structure $\Z$, product of rings.

Ideals and Quotients ideal of a commutative ring, quotient rings, prime ideals, maximal ideals, Chinese remainder theorem.

#### Bilinear and Quadratic Forms Over a Vector Space

Orthogonality orthogonal elements.

Euclidean and Hermitian spaces Euclidean vector spaces, Hermitian vector spaces, dual isomorphism in the euclidean case, orthogonal complement, Cauchy-Schwarz inequality, norm.

#### Affine and Euclidean Geometry

General definitions affine space, affine function, affine subspace, barycenter, affine span.

Euclidean affine spaces angles between vectors.

#### Single Variable Real Analysis

Real numbers definition of $\R$, field structure, order.

Sequences of real numbers convergence, limit point, recurrent sequences, limit infimum and supremum, Cauchy sequences.

Real-valued functions defined on a subset of $\R$ continuity, limits, intermediate value theorem, image of a segment, continuity of monotonic functions, continuity of inverse functions.

Elementary functions (trigonometric, rational, $\exp$, $\log$, etc) polynomial functions, logarithms, exponential, power functions, trigonometric functions, hyperbolic trigonometric functions, inverse trigonometric functions, inverse hyperbolic trigonometric functions.

Integration antiderivative of a continuous function.

Sequences and series of functions uniform convergence, continuity of the limit.

#### Multivariable calculus

Differential equations Grönwall lemma.

#### Probability Theory

Definitions of a probability space probability measure, sigma-algebra, Borel-Cantelli lemma (easy direction).

Random variables and their laws discrete law, Bernoulli law.

Convergence of series of random variables almost surely convergence.