This webpage is about Lean 3, which is effectively obsolete; the community has migrated to Lean 4.
Undergraduate mathematics in mathlib
This gives pointers to undergraduate maths topics that are currently covered in mathlib. The list is gathered from the French curriculum. There is also a page listing undergraduate maths topics that are not yet in mathlib.
To update this list, please submit a PR modifying docs/undergrad.yaml in the mathlib repository.
Linear algebra
Fundamentals vector space, product of vector spaces, vector subspace, quotient space, sum of subspaces, direct sum, complementary subspaces, linear independence, generating sets, bases, existence of bases, linear map, range of a linear map, kernel of a linear map, algebra of endomorphisms of a vector space, general linear group.
Duality dual vector space, dual basis, transpose of a linear map.
Finite-dimensional vector spaces
finite-dimensionality,
isomorphism with
Multilinearity
multilinear map,
determinant of vectors,
determinant of endomorphisms,
orientation of a
Matrices commutative-ring-valued matrices, field-valued matrices, matrix representation of a linear map, change of basis, rank of a matrix, determinant, invertibility.
Endomorphism polynomials annihilating polynomials, minimal polynomial, characteristic polynomial, Cayley-Hamilton theorem.
Structure theory of endomorphisms eigenvalue, eigenvector, generalized eigenspaces.
Linear representations Schur's lemma.
Exponential matrix exponential.
Group Theory
Basic definitions group, group morphism, direct product of groups, subgroup, subgroup generated by a subset, order of an element, normal subgroup, quotient group, group action, stabilizer of a point, orbit, quotient space, class formula, conjugacy classes.
Abelian group cyclic group, finite type abelian groups, complex roots of unity, primitive complex roots of unity.
Permutation group permutation group of a type, decomposition into transpositions, decomposition into cycles with disjoint support, signature, alternating group.
Classical automorphism groups general linear group, special linear group, orthogonal group, unitary group.
Representation theory of finite groups Maschke theorem, orthogonality of irreducible characters, characters of a finite dimensional representation.
Ring Theory
Fundamentals
ring,
subrings,
ring morphisms,
ring structure
Ideals and Quotients ideal of a commutative ring, quotient rings, prime ideals, maximal ideals, Chinese remainder theorem.
Algebra associative algebra over a commutative ring.
Divisibility in integral domains
irreducible elements,
invertible elements,
coprime elements,
unique factorisation domain (UFD),
greatest common divisor,
least common multiple,
Polynomial rings
Field Theory
fields,
characteristic of a ring,
characteristic zero,
characteristic p,
Subfields,
Frobenius morphisms,
field
Bilinear and Quadratic Forms Over a Vector Space
Bilinear forms bilinear forms, alternating bilinear forms, symmetric bilinear forms, nondegenerate forms, matrix representation, change of coordinates.
Quadratic forms quadratic form, polar form of a quadratic.
Orthogonality orthogonal elements, adjoint endomorphism, Gram-Schmidt orthogonalisation.
Euclidean and Hermitian spaces Euclidean vector spaces, Hermitian vector spaces, dual isomorphism in the euclidean case, orthogonal complement, Cauchy-Schwarz inequality, norm, orthonormal bases.
Endomorphisms orthogonal group, unitary group, self-adjoint endomorphism, diagonalization of a self-adjoint endomorphism, decomposition of an orthogonal transformation as a product of reflections.
Low dimensions cross product, triple product.
Affine and Euclidean Geometry
General definitions affine space, affine function, affine subspace, barycenter, affine span, affine groups.
Convexity convex subsets, convex hull of a subset of an affine real space, extreme point.
Euclidean affine spaces isometries of a Euclidean affine space, group of isometries of a Euclidean affine space, angles between vectors, cocyclicity.
Single Variable Real Analysis
Real numbers
definition of
Sequences of real numbers convergence, limit point, recurrent sequences, limit infimum and supremum, Cauchy sequences.
Topology of R
metric structure,
completeness of R,
Bolzano-Weierstrass theorem,
compact subsets of
Numerical series
Geometric series,
convergence of
Real-valued functions defined on a subset of
Differentiability
derivative at a point,
differentiable functions,
derivative of a composition of functions,
derivative of the inverse of a function,
Rolle's theorem,
mean value theorem,
higher order derivatives of functions,
Taylor-like theorems Taylor's theorem with Lagrange form for remainder.
Elementary functions (trigonometric, rational,
Integration Riemann sums, antiderivative of a continuous function, change of variable, integration by parts.
Sequences and series of functions pointwise convergence, uniform convergence, continuity of the limit of a sequence of functions, continuity of the sum of a series of functions, differentiability of the limit of a sequence of functions, differentiability of the sum of a series of functions, Weierstrass polynomial approximation theorem, Weierstrass trigonometric approximation theorem.
Convexity convex functions of a real variable, characterizations of convexity, convexity inequalities.
Single Variable Complex Analysis
Complex Valued series radius of convergence, continuity, differentiability with respect to the complex variable, complex exponential, extension of trigonometric functions to the complex plane(cos, sin), power series expansion of elementary functions(cos, sin).
Functions on one complex variable holomorphic functions, Cauchy formulas, analyticity of a holomorphic function, principle of isolated zeros, principle of analytic continuation, maximum principle, holomorphic stability under uniform convergence.
Topology
Topology and Metric Spaces topology of a metric space, induced topology, finite product of metric spaces, limits of sequences, cluster points, continuous functions, homeomorphisms, compactness in terms of open covers (Borel-Lebesgue), sequential compactness is equivalent to compactness (Bolzano-Weierstrass), connectedness, connected components, path connectedness, Lipschitz functions, uniformly continuous functions, Heine-Cantor theorem, complete metric spaces, contraction mapping theorem.
Normed vector spaces on
Hilbert spaces
Hilbert projection theorem,
orthogonal projection onto closed vector subspaces,
dual space,
Riesz representation theorem,
inner product space
Multivariable calculus
Differential calculus
differentiable functions on an open subset of
Differential equations Cauchy-Lipschitz Theorem, Grönwall lemma.
Measures and integral calculus
Measure theory measurable spaces, sigma-algebras, product of sigma-algebras, Borel sigma-algebras, positive measure, counting measure, Lebesgue measure, product measure, measurable functions, approximation by step functions.
Integration
integral of positive measurable functions,
monotone convergence theorem,
Fatou's lemma,
integrable functions,
dominated convergence theorem,
finite dimensional vector-valued integrable functions,
continuity of integrals with respect to parameters,
Fourier analysis Fourier series of locally integrable periodic real-valued functions, Riemann-Lebesgue lemma, Parseval theorem.
Probability Theory
Definitions of a probability space
probability measure,
events,
independent events,
sigma-algebra,
independent sigma-algebra,
Random variables and their laws discrete law, probability density function, independence of random variables, mean of a random variable, variance of a real-valued random variable, moments, Bernoulli law.
Convergence of a sequence of random variables
convergence in probability,
Distribution calculus
Spaces
Numerical Analysis
Approximation of numerical functions Lagrange interpolation, Lagrange polynomial of a function at (n + 1) points.