The shared library
Theorem library
Every result in the canon, grouped by unit. Press ⌘K to search.
135
theorems
25
units
6
threads
MU-101 · Foundations & Mathematical Proof 7
| T-001 | If a statement holds for 1 and its truth at n forces its truth at n+1, it holds for every natural number. | |
| T-002 | Every non-empty set of natural numbers has a least element, and this is equivalent to induction. | |
| T-003 | If n+1 objects are placed in n boxes, some box holds at least two. | |
| T-004 | No ratio of integers squares to 2; the proof is the classic argument by contradiction. | |
| T-005 | There is no largest prime; assuming a finite list yields a contradiction. | |
| T-006 | No list can enumerate all real numbers — Cantor's diagonal argument. | |
| T-007 | A set never has the same cardinality as its power set: |P(A)| > |A|. |
MU-102 · Calculus I 7
| T-008 | The derivative of a composition is the product of the derivatives. | |
| T-009 | A differentiable function equal at two points has a stationary point between them. | |
| T-010 | A differentiable function attains its average rate of change at some interior point. | |
| T-011 | A continuous function on a closed interval attains a maximum and a minimum. | |
| T-012 | Differentiation and integration are inverse operations. | |
| T-013 | A smooth function equals its Taylor polynomial plus a controllable error term. | |
| T-014 | Indeterminate limits of ratios can be resolved by differentiating numerator and denominator. |
MU-103 · Linear Algebra I 6
| T-015 | For a linear map, rank plus nullity equals the dimension of the domain. | |
| T-016 | A dozen conditions on a square matrix are all equivalent to invertibility. | |
| T-017 | det(AB) = det(A)det(B). | |
| T-018 | The inner product of two vectors is bounded by the product of their norms. | |
| T-019 | Any basis can be turned into an orthonormal one. | |
| T-020 | Solutions of a square linear system as ratios of determinants. |
MU-104 · Analysis I — Sequences & Series 7
| T-021 | Limits respect sums, products, and quotients. | |
| T-022 | A sequence trapped between two convergents to L also converges to L. | |
| T-023 | A bounded monotone sequence converges. | |
| T-024 | Every bounded sequence has a convergent subsequence. | |
| T-025 | A sequence of reals converges if and only if it is Cauchy. | |
| T-026 | A series converges absolutely when the limiting ratio of terms is below one. | |
| T-027 | An alternating series with terms decreasing to zero converges. |
MU-105 · Discrete Mathematics 6
| T-028 | An expansion of (x+y)^n in terms of binomial coefficients. | |
| T-029 | The size of a union from the sizes of intersections. | |
| T-030 | In any graph the sum of degrees is twice the number of edges. | |
| T-031 | a^p ≡ a (mod p) for prime p. | |
| T-032 | Congruences with coprime moduli have a unique joint solution. | |
| T-033 | A connected graph has an Eulerian circuit iff every vertex has even degree. |
MU-106 · Probability I 6
| T-034 | Probability of an event via a partition of the sample space. | |
| T-035 | How to invert conditional probabilities. | |
| T-036 | Expectation of a sum is the sum of expectations, dependence notwithstanding. | |
| T-037 | A tail bound from the mean alone for non-negative variables. | |
| T-038 | A tail bound from the variance. | |
| T-039 | Sample means converge in probability to the expectation. |
MU-201 · Real Analysis 6
| T-040 | A continuous function takes every value between two of its values. | |
| T-041 | A subset of R^n is compact iff it is closed and bounded. | |
| T-042 | Continuous on a compact set implies uniformly continuous. | |
| T-043 | A bounded function is integrable iff upper and lower sums can be made arbitrarily close. | |
| T-044 | A uniform limit of continuous functions is continuous. | |
| T-045 | A dominated series of functions converges uniformly. |
MU-202 · Linear Algebra II 6
| T-046 | Every basis of a vector space has the same cardinality. | |
| T-047 | A self-adjoint operator has an orthonormal basis of eigenvectors. | |
| T-048 | Every matrix satisfies its own characteristic polynomial. | |
| T-049 | Every operator over C is similar to a direct sum of Jordan blocks. | |
| T-050 | Any matrix factors as a rotation, a scaling, and a rotation. | |
| T-051 | Best approximation in an inner product space is orthogonal projection. |
MU-203 · Multivariable & Vector Calculus 5
| T-052 | How volumes transform under a smooth change of coordinates. | |
| T-053 | Constrained extrema occur where gradients align. | |
| T-054 | A planar circulation integral equals a double integral of curl. | |
| T-055 | Circulation around a boundary equals the flux of curl through the surface. | |
| T-056 | Flux through a closed surface equals the integral of divergence inside. |
MU-204 · Group Theory 6
| T-057 | The order of a subgroup divides the order of the group. | |
| T-058 | Orbit size times stabiliser size equals the group order. | |
| T-059 | The image of a homomorphism is the quotient by its kernel. | |
| T-060 | If a prime divides the group order, an element of that order exists. | |
| T-061 | Existence, conjugacy, and counting of maximal p-subgroups. | |
| T-062 | Every finite abelian group is a product of cyclic groups. |
MU-205 · Ordinary Differential Equations 5
| T-063 | A Lipschitz ODE has a unique local solution. | |
| T-064 | Solutions of a linear equation form a vector space. | |
| T-065 | A non-vanishing Wronskian certifies linear independence of solutions. | |
| T-066 | A particular solution from the homogeneous solutions. | |
| T-067 | Eigenvalues of the linearisation classify equilibria. |
MU-206 · Complex Analysis 6
| T-068 | Complex differentiability is equivalent to a pair of PDEs. | |
| T-069 | The integral of a holomorphic function round a closed loop is zero. | |
| T-070 | A holomorphic function's values are determined by its boundary values. | |
| T-071 | A bounded entire function is constant. | |
| T-072 | Every non-constant polynomial over C has a root. | |
| T-073 | A contour integral equals the sum of enclosed residues. |
MU-207 · Number Theory 5
| T-074 | The gcd is an integer combination of its arguments. | |
| T-075 | Every integer factors uniquely into primes. | |
| T-076 | a^φ(n) ≡ 1 (mod n) for a coprime to n. | |
| T-077 | (p−1)! ≡ −1 (mod p) exactly when p is prime. | |
| T-078 | A reciprocal relationship between two primes being squares mod each other. |
MU-301 · Metric & Topological Spaces 5
| T-079 | A map is continuous iff preimages of open sets are open. | |
| T-080 | Open-cover and sequential compactness coincide in metric spaces. | |
| T-081 | A contraction on a complete space has a unique fixed point. | |
| T-082 | A complete metric space is not a countable union of nowhere-dense sets. | |
| T-083 | An arbitrary product of compact spaces is compact. |
MU-302 · Measure & Integration 5
| T-084 | A premeasure extends to a genuine measure. | |
| T-085 | Integrals commute with increasing limits of non-negative functions. | |
| T-086 | The integral of a liminf is at most the liminf of integrals. | |
| T-087 | A dominated pointwise limit may be integrated term by term. | |
| T-088 | When iterated integrals may be exchanged. |
MU-303 · Rings, Fields & Galois Theory 6
| T-089 | Principal ideal domains have unique factorisation. | |
| T-090 | A prime-based test for irreducibility of polynomials. | |
| T-091 | Degrees of field extensions multiply. | |
| T-092 | Subfields correspond to subgroups of the Galois group. | |
| T-093 | There is exactly one field of each prime-power order. | |
| T-094 | No general radical formula solves degree-five equations. |
MU-304 · Functional Analysis 5
| T-095 | Bounded functionals extend without increasing norm. | |
| T-096 | A surjective bounded operator between Banach spaces is open. | |
| T-097 | A closed-graph operator between Banach spaces is bounded. | |
| T-098 | Pointwise-bounded families of operators are uniformly bounded. | |
| T-099 | Every bounded functional on a Hilbert space is an inner product. |
MU-305 · Partial Differential Equations 5
| T-100 | Reducing a PDE to ODEs via product solutions. | |
| T-101 | The 1D wave equation solved by travelling waves. | |
| T-102 | A harmonic function attains its extrema on the boundary. | |
| T-103 | When and how a periodic function equals its Fourier series. | |
| T-104 | First-order PDEs solved along characteristic curves. |
MU-306 · Differential Geometry 4
| T-105 | Curvature and torsion determine a space curve. | |
| T-106 | Lengths and angles on a surface from its metric. | |
| T-107 | Gaussian curvature is intrinsic to the surface. | |
| T-108 | Total curvature is a topological invariant. |
MU-307 · Combinatorics & Graph Theory 5
| T-109 | Complete disorder is impossible in large enough structures. | |
| T-110 | A matching exists iff every set of vertices has enough neighbours. | |
| T-111 | Maximum flow equals minimum cut capacity. | |
| T-112 | A graph is planar unless it contains K5 or K3,3. | |
| T-113 | The maximum edges in a graph with no large clique. |
MU-308 · Numerical Analysis 4
| T-114 | Contraction guarantees convergence of iterative schemes. | |
| T-115 | Quadratic convergence near a simple root. | |
| T-116 | The unique interpolating polynomial and its remainder. | |
| T-117 | Optimal node placement integrates high-degree polynomials exactly. |
MU-401 · Algebraic Topology 4
| T-118 | Loops up to homotopy form a group invariant of the space. | |
| T-119 | The fundamental group of a union from those of its pieces. | |
| T-120 | Every continuous self-map of a disc has a fixed point. | |
| T-121 | V−E+F is a topological invariant. |
MU-402 · Representation Theory 4
| T-122 | Representations of finite groups over C are completely reducible. | |
| T-123 | Morphisms between irreducibles are zero or isomorphisms. | |
| T-124 | Irreducible characters form an orthonormal set. | |
| T-125 | Orbits counted by average fixed points. |
MU-403 · Logic & Set Theory 5
| T-126 | Every chain-bounded poset has a maximal element — equivalent to choice. | |
| T-127 | A theory is satisfiable iff every finite subset is. | |
| T-128 | First-order theories with infinite models have models of every infinite size. | |
| T-129 | Every logically valid first-order formula is provable. | |
| T-130 | Sufficiently strong consistent systems cannot prove their own consistency. |
MU-404 · Measure-Theoretic Probability 5
| T-131 | When infinitely many events occur, almost surely or not. | |
| T-132 | Sample means converge almost surely to the mean. | |
| T-133 | Sums of independent variables are asymptotically Gaussian. | |
| T-134 | Conditioning is orthogonal projection in L2. | |
| T-135 | A bounded martingale converges almost surely. |