# 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,
rank of a set of vectors,
isomorphism with bidual.

**Multilinearity**
multilinear map,
determinant of vectors,
determinant of endomorphisms,
orientation of a $\R$-vector space.

**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**
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,
Bézout's identity,
$\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,
rational fraction fields with one indeterminate over a 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.

**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,
diagonalization of a self-adjoint endomorphism,
decomposition of an orthogonal transformation as a product of reflections.

**Low dimensions**
cross 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.

#### 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,
rational 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 space $l^2$,
its completeness,
inner product space $L^2$,
Hilbert bases,
example, the Hilbert basis of trigonometric polynomials.

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

**Fourier analysis**
Parseval 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,
Markov inequality.