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.
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.
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.
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
Orthogonality orthogonal elements.
Endomorphisms self-adjoint endomorphism.
Affine and Euclidean Geometry
Euclidean affine spaces angles between vectors.
Single Variable Real Analysis
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.
Single Variable Complex Analysis
Complex Valued series radius of convergence, continuity, complex exponential, extension of trigonometric functions to the complex plane.
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.
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.
Convergence of series of random variables almost surely convergence.