# 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 $K^n$,
rank of a linear map,
isomorphism with bidual.

**Multilinearity**
multilinear map,
determinant of vectors,
determinant of endomorphisms.

**Matrices**
commutative-ring-valued matrices,
field-valued matrices,
matrix representation of a linear map,
change of basis,
determinant,
invertibility.

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

**Structure theory of endomorphisms**
eigenvalue,
eigenvector,
generalized eigenspaces.

#### 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,
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.

#### 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.

**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,
$A[X]$ is a UFD when $A$ is a UFD,
principal ideal domain,
Euclidean rings,
Euclid's' algorithm,
$\Z$ is a euclidean ring,
congruence in $\Z$,
prime numbers,
$\Z/n\Z$ and its invertible elements,
Euler's totient function ($\varphi$).

**Polynomial rings**
$K[X]$ is a euclidean ring when $K$ is a field,
irreducible polynomial,
cyclotomic polynomials in $\Q[X]$,
Eisenstein's criterion,
polynomial algebra in one or several indeterminates over a commutative ring,
roots of a polynomial,
multiplicity,
polynomial derivative,
decomposition into sums of homogeneous polynomials,
symmetric polynomials.

**Field Theory**
fields,
characteristic of a ring,
characteristic zero,
characteristic p,
Subfields,
Frobenius morphisms,
field $\Q$ of rational numbers,
field $\R$ of real numbers,
field $\C$ of complex numbers,
$\C$ is algebraically closed,
field of fractions of an integral domain,
algebraic elements,
transcendental elements,
algebraic extensions,
algebraically closed fields,
rupture fields,
splitting fields,
finite fields.

#### 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,
Sylvester's law of inertia.

**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**
self-adjoint endomorphism.

#### Affine and Euclidean Geometry

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

**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.

#### 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.

**Topology of R**
metric structure,
completeness of R,
Bolzano-Weierstrass theorem,
compact subsets of $\R$,
connected subsets of $\R$,
additive subgroups of $\R$.

**Numerical series**
Geometric series,
convergence of $p$-series for $p>1$.

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

**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,
$C^k$ functions,
Leibniz formula.

**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,
integration by parts.

**Sequences and series of functions**
uniform convergence,
continuity of the limit,
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.

#### 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 $\R$ and $\C$**
topology on a normed vector space,
Banach open mapping theorem,
equivalence of norms in finite dimension,
norms $\lVert\cdot\rVert_p$ on $\R^n$ and $\C^n$,
absolutely convergent series in Banach spaces,
continuous linear maps,
norm of a continuous linear map,
uniform convergence norm (sup-norm),
normed space of bounded continuous functions,
its completeness,
Heine-Borel theorem (closed bounded subsets are compact in finite dimension),
Riesz' lemma (unit-ball characterization of finite dimension),
Arzela-Ascoli theorem.

**Hilbert spaces**
Hilbert projection theorem,
orthogonal projection onto closed vector subspaces,
dual space,
Riesz representation theorem,
inner product spaces $l^2$ and $L^2$,
their completeness,
Hilbert bases, i.e. complete orthonormal sets (in the separable case),
example, the Hilbert basis of trigonometric polynomials,
its orthonormality,
its completeness.

#### Multivariable calculus

**Differential calculus**
differentiable functions on an open subset of $\R^n$,
differentials (linear tangent functions),
chain rule,
mean value theorem,
differentiable functions,
$k$-times continuously differentiable functions,
partial derivatives commute,
local extrema,
convexity of functions on an open convex subset of $\R^n$,
diffeomorphisms,
inverse function theorem,
implicit function theorem.

**Differential equations**
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,
$\mathrm{L}^p$ spaces where $1 ≤ p ≤ ∞$,
Completeness of $\mathrm{L}^p$ spaces,
Holder's inequality,
Fubini's theorem.

#### Probability Theory

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

**Random variables and their laws**
discrete law,
independence of random variables,
Bernoulli law.

**Convergence of series of random variables**
almost surely convergence.