Explore Cumulus

Cumulus is the Grace17 mathematics library. Search names and statements, follow imports, and open any declaration in the browser proof assistant.

Loading declaration index…

Modules by area

Kernel and bootstrap 12 modules · 96 declarations

The axioms, ordered pairs, the natural numbers, lists and trees, and the syntax everything else is written in.

Sets, relations, and functions 38 modules · 636 declarations

Set algebra, power sets and families, relations and their algebra, functions, images, orders, well-orders, choice, Zorn's lemma, and the well-ordering theorem.

Ordinals and cardinals 41 modules · 647 declarations

Transfinite recursion, ordinal arithmetic, order types, Hartogs' theorem, finiteness and counting, countability, dominance, and infinite cardinal arithmetic.

Natural numbers, integers, and rationals 41 modules · 1,000 declarations

Arithmetic and order on ℕ with its everyday lemmas, the construction of ℤ with its order, signs, parity, and absolute value, the construction of ℚ, division, and the least-number principle.

Real analysis 32 modules · 829 declarations

Sequences, continuity, the intermediate and extreme value theorems, differentiation, Riemann integration, and the fundamental theorem of calculus.

Real numbers 43 modules · 686 declarations

The Dedekind reals: field and order structure, absolute value, the metric, square roots, uncountability, and the embedding of the rationals.

Complex numbers 29 modules · 253 declarations

The complex field, continuity and compactness in the plane, and the fundamental theorem of algebra.

Groups 36 modules · 891 declarations

Bundled groups with a * b and a⁻¹, subgroups, cosets and Lagrange's theorem, homomorphisms f : G →* H, kernels, normal subgroups and quotients, the first isomorphism theorem, products, cyclic subgroups and element orders, and centers.

Rings and ideals 66 modules · 858 declarations

Rings, ideals, quotients, prime and maximal ideals, determinants over rings, and the isomorphism theorems.

Fields 21 modules · 145 declarations

Fields and ordered fields, localisation, and integral descent.

Polynomials 70 modules · 599 declarations

Polynomial rings, Horner evaluation, roots and factors, variables, and the Nullstellensatz.

Modules and coefficients 33 modules · 305 declarations

Coefficient maps, indexed lists, spans and annihilators, finite module towers, and integral extensions.

Linear algebra 8 modules · 262 declarations

Vectors, matrices, determinants, and spans.

Number theory 36 modules · 646 declarations

Divisibility, Bézout, the Euclidean algorithm, prime factorisation, modular arithmetic, the Chinese remainder theorem, Fermat, Euler, and Wilson.

Combinatorics 35 modules · 866 declarations

Inclusion–exclusion, the pigeonhole principle, binomial identities, counting functions, injections, and permutations, Fibonacci, Lucas, Catalan, Stirling, and Bell numbers, the infinite Ramsey theorem, and Möbius inversion.

Probability 11 modules · 256 declarations

Finite probability spaces, events, uniform distributions, conditional probability and Bayes, independence, random variables, expectation and variance, and the Markov and Chebyshev inequalities.

Geometry 45 modules · 584 declarations

Coordinate geometry over the reals: distances, triangles, and the classical theorems.

Graph theory 61 modules · 1,003 declarations

Graphs, walks, Eulerian trails, and shortest paths.

Lists 17 modules · 385 declarations

Lists as finite sequences: indexing, concatenation, reversal, take and drop, filtering, counts and permutations, sums, prefixes, sorting, and the bridge to functions on a natural number.

Topology 30 modules · 610 declarations

Topological spaces, continuous maps, compactness, subspaces, separation, the standard topology on the line, and Heine–Borel.

Metric spaces 17 modules · 433 declarations

Metrics and balls, the metric topology, closed sets and closure, ε–δ continuity, Lipschitz maps and isometries, Cauchy sequences and completeness, boundedness, and the real line, discrete, subspace, and product metrics.

Fixed point theorems 31 modules · 449 declarations

Knaster–Tarski on subsets, the fixed point theorem on a closed interval, Kuhn's lemma, and Brouwer's theorem for the cube and for products of simplices.

Game theory 6 modules · 87 declarations

Mixed strategy profiles on products of simplices, expected payoffs, Nash's map, and the existence of Nash equilibria.

Lattices 26 modules · 806 declarations

Ordered sets bundled as one set P with a ⊑ b, a ⊔ b, a ⊓ b, bot(P), top(P), and sSup(P)(S) read off the hypothesis: suprema and infima, lattices and their laws, bounded, complete, distributive, modular, and Boolean lattices, the powerset lattice, monotone maps and Galois connections, Knaster–Tarski on complete lattices, homomorphisms, sublattices, ideals, and filters.

Category theory 13 modules · 482 declarations

Small categories as bundled sets with hom-typed morphisms, isomorphisms, monomorphisms and epimorphisms, terminal and initial objects, functors F : C ⥤ D, natural transformations, opposite categories, products, example categories including the category of sets below a universe, hom functors, and the Yoneda lemma.

Library roots 8 modules · 233 declarations

The modules that import whole areas, so one import brings a subject in.