Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
A Maximiser of the Quadratic Form of a Symmetric Matrix on Unit Vectors Orthogonal to Given Eigenvectors Is an Eigenvector
lemmalem:symmetric-maximiser-eigenvector-2026aLinear AlgebraFor a real symmetric matrix and finitely many (fewer than n) orthonormal eigenvectors, the quadratic form attains a maximum on the unit vectors orthogonal to them, and every maximiser is an eigenvector whose eigenvalue is the maximum value.Rules for Orthogonal Matrices: Inverse, Products, Isometry, Columns, Determinant, Orthonormal Extension and Expansion
lemmalem:orthogonal-matrix-rules-2026aLinear AlgebraAn orthogonal matrix is invertible with inverse its transpose; orthogonal matrices contain the identity and are closed under products; they preserve dot products and norms; a matrix is orthogonal exactly when its columns are orthonormal; the determinant is 1 or -1; fewer than n p…Real Eigenvalues and Eigenvectors of a Real Square Matrix
definitiondef:eigenvalue-eigenvector-real-matrix-2026aLinear AlgebraA nonzero point x of R^n is an eigenvector of a square real matrix A with eigenvalue lambda if Ax = lambda x; a real number lambda is an eigenvalue of A if A has an eigenvector with eigenvalue lambda.- For a point lambda of R^n, diag(lambda) is the n x n real matrix with lambda_i in the (i,i) entry and 0 off the diagonal.
- A square real matrix Q is orthogonal if its transpose times Q is the identity matrix; O(n) is the set of orthogonal n x n matrices.
Rules for Symmetric and Positive Semidefinite Matrices: Closure, Self-Adjointness, Polarization, Congruence and Cones
lemmalem:symmetric-psd-matrix-rules-2026aLinear AlgebraSymmetric matrices are closed under the linear operations, are self-adjoint for the dot product, are determined by their quadratic forms and are preserved by congruence; positive semidefinite and positive definite matrices form cones that congruence preserves.Predicative Formulas for Suprema and Infima, and Maps Defined by Suprema and Infima
helperhlp:order-bound-formulas-predicative-2026aSet TheoryBeing the supremum, or the infimum, of a subset of a partially ordered set is expressed by explicit predicative formulas, so that suprema and infima can be substituted into predicative formulas and used to define maps.Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices
settingset:routine-facts-2026bAnalysisSet TheoryExtends the metric-spaces setting by carrying, by reference, the routine facts on arithmetic and closure in the real and complex numbers, on maps given by expressions and operations, on the predicativity of formulas and on index sets, so that adopters use them without citation.Predicative Formulas for Convergence and Limits, and Maps Defined by Limits
helperhlp:limit-formulas-predicative-2026aAnalysisSet TheoryConvergence of a sequence in a metric space to a point is expressed by an explicit predicative formula, which makes the limit a defined set symbol that can be substituted into predicative formulas and used to define maps; for the real line the formula agrees with convergence of r…Values, Restriction and Equality of a Map, and the Map as a Defined Set Symbol
helperhlp:map-values-2026aSet TheoryFor a map f from A to B: (a,b) lies in f exactly when f(a)=b, (a,f(a)) lies in f with f(a) in B, the restriction of f to A is f, and maps from A to B with equal values are equal; and a map u to t(u,v) given by an expression is the unique set satisfying a predicative formula, so i…Natural Numbers as Indices: ℕ ⊆ ℕ₀, 1 ∈ ℕ₀, and the Two Readings of an Operation from 1 to n
helperhlp:natural-number-index-facts-2026aSet TheoryEvery natural number lies in the natural numbers with zero, 1 lies in both, and for an associative and commutative operation the iterated operation from 1 to n, read along [n] or over the interval, equals the operation over the finite set [n].- For all real numbers x, y and z, the closure, commutative, associative, distributive, neutral, negative and zero-product laws, the four laws of the total order, and that |x| is a nonnegative real number.
Extending a Permutation of [n-1] to a Permutation of [n] with a Prescribed Value, and Its Sign
lemmalem:permutation-extension-2026aCombinatoricsSet TheoryFor i in [n], sending a pair (j, tau) with j in [n] and tau a permutation of [n-1] to the permutation of [n] that maps i to j and acts as tau through the deletion index maps is a bijection onto the permutations of [n], and it multiplies the sign by (-1)^(i+j).- For n at least 2 and i in [n], the deletion index map s_i from [n-1] to [n] keeps the numbers below i and raises the others by one, skipping i.
- For n at least 2 and i in [n], there is exactly one map from [n-1] to [n] fixing the numbers below i and shifting the others up by one; it is strictly increasing and a bijection onto [n] without i.
Expanding a Product of Sums over a Fixed Finite Index Set
lemmalem:product-of-sums-expansion-2026aAlgebraFor finite sets A and B and a map u from A x B to a commutative ring, the product over A of the sums over B of u equals the sum, over all maps from A to B, of the products of u along the map; the term maps of both sides exist.- An inversion of a permutation σ of [n] is a pair (i,j) with i<j and σ(j)<σ(i); Inv(σ) is the set of its inversions.
Cofactor Expansion of the Determinant along a Row or a Column, and the Adjugate Identity
lemmalem:determinant-laplace-expansion-2026aLinear AlgebraFor a square real matrix of size at least two, the determinant is the sum of the entries of any row, or of any column, times their cofactors, and the product of the matrix with its adjugate, in either order, is the determinant times the identity matrix.A Square Real Matrix Is Invertible if and only if Its Determinant Is Nonzero
theoremthm:determinant-invertibility-2026aLinear AlgebraA square real matrix is invertible exactly when its determinant is nonzero, and then the determinant of the inverse is the reciprocal of the determinant.The Determinant Map and the Matrices Formed from a Square Matrix by Reindexing Rows, Replacing a Row and Deleting a Row and a Column Exist and Are Unique
lemmalem:determinant-existence-2026aLinear AlgebraFor a square real matrix A, the Leibniz terms sgn(σ) times the product of the entries A_{iσ(i)} form a map on the permutations, and summing them gives a map on square matrices. The matrices obtained from A by reindexing its rows, replacing one row, and deleting one row and one co…