Missing undergraduate mathematics in mathlib

This gives pointers to undergraduate maths topics that are currently missing in mathlib. The list is gathered from the French curriculum. There is also a page listing undergraduate maths topics that are already in mathlib.

If you want to work on an item from this list then you should first check the pull requests list to see whether it is already coming, then the issues list to see whether it is discussed there, and finally talk about this idea on Zulip.

Linear algebra

Duality: orthogonality.

Finite-dimensional vector spaces: rank of a set of vectors, rank of a system of linear equations.

Multilinearity: determinant of endomorphisms, special linear group, orientation of a $\R$-valued vector space.

Matrices: change of basis, rank of a matrix, elementary row operations, elementary column operations, Gaussian elimination, row-reduced matrices.

Endomorphism polynomials: annihilating polynomials.

Structure theory of endomorphisms: diagonalization, triangularization, invariant subspaces of an endomorphism, kernels lemma, Dunford decomposition, Jordan normal form.

Linear representations: irreducible representation, Schur's lemma, examples.

Exponential: endomorphism exponential, matrix exponential.

Group Theory

Basic definitions: class formula.

Abelian group: finite type abelian groups.

Classical automorphism groups: special orthogonal group, special unitary group.

Representation theory of finite groups: representations of abelian groups, dual groups, Maschke theorem, orthogonality of irreducible characters, Fourier transform for finite abelian groups, convolution, class function over a group, characters of a finite dimensional representation, orthonormal basis of irreducible characters, examples of groups with small cardinality.

Ring Theory

Algebra: algebra over a commutative ring.

Divisibility in integral domains: Bezout's identity.

Polynomial rings: relationship between the coefficients and the roots of a split polynomial, Newton's identities.

Field Theory: transcendental elements, rational fraction fields with one indeterminate over a field, $\R(X)$-partial fraction decomposition, $\C(X)$-partial fraction decomposition.

Bilinear and Quadratic Forms Over a Vector Space

Bilinear forms: rank of a bilinear form.

Orthogonality: Sylvester's law of inertia, real classification, complex classification, Gram-Schmidt orthogonalisation.

Endomorphisms: orthogonal group, unitary group, special orthogonal group, special unitary group, normal endomorphism, diagonalization of a self-adjoint endomorphism, diagonalization of normal endomorphisms, simultaneous diagonalization of two real quadratic forms, with one positive-definite, decomposition of an orthogonal transformation as a product of reflections, polar decompositions in $\mathrm{GL}(n, \R)$, polar decompositions in $\mathrm{GL}(n, \C)$.

Low dimensions: cross product, triple product, classification of elements of $\mathrm{O}(2, \R)$, classification of elements of $\mathrm{O}(3, \R)$.

Affine and Euclidean Geometry

General definitions: equations of affine subspace, affine groups, affine property, group generated by homotheties and translations, transformations fixing a basis of directions.

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, isometries that do and do not preserve orientation, direct and opposite similarities of the plane, classification of isometries in two and three dimensions, angles between planes, inscribed angle theorem, cocyclicity, group of isometries stabilizing a subset of the plane or of space, regular polygons, metric relations in the triangle, using complex numbers in plane geometry.

Application of quadratic forms to study proper conic sections of the affine euclidean plane: focus, eccentricity, quadric surfaces in 3-dimensional Euclidean affine spaces.

Single Variable Real Analysis

Numerical series: Convergence of real valued-series, positive valued series, summation of comparison relations, comparison of a series and an integral, error estimation, absolute convergence, products of series, alternating series.

Differentiability: piecewise $C^k$ functions.

Taylor-like theorems: Taylor's theorem with little-o remainder, Taylor's theorem with integral form for remainder, Taylor's theorem with Lagrange form for remainder, Taylor series expansions.

Elementary functions (trigonometric, rational, $\exp$, $\log$, etc): rational functions.

Integration: integral over a segment of piecewise continuous functions, antiderivatives, Riemann sums, change of variable, improper integrals, absolute vs conditional convergence of improper integrals, comparison test for improper integrals.

Sequences and series of functions: pointwise convergence, normal convergence, differentiability of the limit, Weierstrass polynomial approximation theorem, Weierstrass trigonometric approximation theorem.

Convexity: continuity and differentiability of convex functions.

Single Variable Complex Analysis

Complex Valued series: antiderivative, power series expansion of elementary functions.

Functions on one complex variable: holomorphic functions, Cauchy-Riemann conditions, contour integrals of continuous functions in $\C$, antiderivatives of a holomorphic function, representations of the $\log$ function on $\C$, theorem of holomorphic functions under integral domains, winding number of a closed curve in $\C$ with respect to a point, Cauchy formulas, analyticity of a holomorphic function, principle of isolated zeros, principle of analytic continuation, maximum principle, isolated singularities, Laurent series, meromorphic functions, residue theorem, sequences and series of holomorphic functions, holomorphic stability under uniform convergence.


Normed vector spaces on $\R$ and $\C$: equivalent norms, Riesz' lemma (unit-ball characterization of finite dimension).

Hilbert Spaces: Hilbert basis of trigonometric polynomials, Hilbert bases of orthogonal polynomials, Lax-Milgram theorem, $H^1_0([0,1])$ and its application to the one-dimensional Dirichlet problem.

Multivariable calculus

Differential Calculus: directional derivative, partial derivatives, Jacobian matrix, gradient vector, Hessian matrix, $k$-th order partial derivatives, partial derivatives commute, Taylor's theorem with little-o remainder, Taylor's theorem with integral form for remainder.

Differential equations: Cauchy-Lipschitz Theorem, maximal solutions, exit theorem of a compact subspace, autonomous differential equations, phase portraits, qualitative behavior, stability of equilibrium points (linearisation theorem), linear differential systems, method of constant variation (Duhamel’s formula), constant coefficient case, solving systems of differential equations of order $> 1$.

Submanifolds of $\R^n$: local graphs, local parameterization, local equation, tangent space, position with respect to the tangent plane, gradient, line integral, curve length, Lagrange multipliers.

Measures and integral Calculus

Integration: continuity of integrals with respect to parameters, differentiability of integrals with respect to parameters, change of variables for multiple integrals, change of variables to polar co-ordinates, change of variables to spherical co-ordinates, convolution, regularization and approximation by convolution.

Fourier Analysis: Fourier series of locally integrable periodic real-valued functions, Riemann-Lebesgue lemma, convolution product of periodic functions, Dirichlet theorem, Fejer theorem, Parseval theorem, Fourier transforms on $\mathrm{L}^1(\R^d)$ and $\mathrm{L}^2(R^d)$, Plancherel’s theorem.

Probability Theory

Definitions of a probability space: events, $0$-$1$ law, Borel-Cantelli lemma (difficult direction), conditional probability, law of total probability.

Random variables and their laws: absolute continuity of probability laws, probability density function, law of joint probability, mean and variance of a real-valued random variable, transfer theorem, moments, binomial law, geometric law, Poisson law, uniform law, exponential law, Gaussian law, characteristic function, probability generating functions, applications of probability generating functions to sums of independent random variables.

Convergence of series of random variables: convergence in probability, $\mathrm{L}^p$ convergence, Markov inequality, Tchebychev inequality, Levy's theorem, weak law of large numbers, strong law of large numbers, central limit theorem.

Distribution calculus

Spaces $\mathcal{D}(\R^d)$: smooth functions with compact support on $\R^d$, stability by derivation, stability by multiplication by a smooth function, partitions of unity, constructing approximations of probability density functions in spaces of common functions (trig, exp, rational, log, etc).

Distributions on $\R^d$: definition of distributions, locally integrable functions, dirac measures, Cauchy principal values, multiplication by a smooth function, probability distribution function from a dataset, convergent distribution series, support of a distribution.

Spaces $\mathcal{S}(\R^d)$: Schwartz space of rapidly decreasing functions, stability by derivation, stability by multiplication by a slowly growing smooth function, gaussian functions, Fourier transforms on $\mathcal{S}(\R^d)$, convolution of two functions of $\mathcal{S}(\R^d)$.

Tempered distributions: definition, derivation of tempered distributions, multiplication by a function $C^\infty$ of slow growth, $L^2$ functions and Riesz representation, $L^p$ functions, periodic functions, Dirac comb, Fourier transforms, inverse Fourier transform, Fourier transform and derivation, Fourier transform and convolution product.

Applications: Poisson’s formula, using convolution and Fourier-Laplace transform to solve one dimensional linear differential equations, weak solution of partial derivative equation, fundamental solution of the Laplacian, solving the Laplace equations, heat equations, wave equations.

Numerical Analysis

Solving systems of linear inequalities: conditioning, Gershgorin-Hadamard theorem, Gauss’s pivot, LU decomposition.

Iterative methods: Jacobian, Gauss-Seidel, convergence analysis, spectral ray, singular value decomposition, example of discretisation matrix by finite differences of the laplacian in one dimension.

Iterative methods of solving systems of real and vector valued equations: linear systems case, proper element search, brute force method, optimization of convex function in finite dimension, gradient descent square root, nonlinear problems with real and vector values, bisection method, Picard method, Newton’s method, rate of convergence and estimation of error.

Numerical integration: Rectangle method, error estimation, Monte-Carlo method, rate of convergence, application to the calculation of multiple integrals.

Approximation of numerical functions: Lagrange interpolation, Lagrange polynomial of a function at (n + 1) points, estimation of the error.

Ordinary differential equations: numerical aspects of Cauchy's problem, explicit Euler method, consistency, stability, convergence, order.

Fourier transform: discrete Fourier transform on a finite abelian group, fast Fourier transform.