# Undergraduate mathematics in mathlib

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

**Fundamentals**
vector space,
product of vector spaces,
vector subspace,
quotient space,
sum of subspaces,
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.

**Matrices**
commutative-ring-valued matrices,
field-valued matrices,
matrix representation of a linear map,
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,
conjugacy classes.

**Abelian group**
cyclic group,
complex roots of unity,
primitive complex roots of unity.

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

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

**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,
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,
matrix representation,
change of coordinates.

**Quadratic forms**
quadratic form,
polar form of a quadratic.

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

**Endomorphisms**
self-adjoint endomorphism.

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

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

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

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

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

**Convexity**
convex functions of a real variable,
characterizations of convexity,
convexity inequalities.

#### Single Variable Complex Analysis

**Complex Valued series**
radius of convergence,
continuity,
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 normed-space-valued functions,
its completeness,
Heine-Borel theorem (closed bounded subsets are compact in finite dimension),
Arzela-Ascoli theorem.

**Hilbert Spaces**
Hilbert projection theorem,
orthogonal projection onto closed vector subspaces,
dual space,
Riesz representation theorem.

#### 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,
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,
Holder's inequality,
Fubini's theorem.

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