Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
The Eigenvalues of an Operator with an Orthonormal Eigenbasis
lemmalem:eigenvalues-orthonormal-eigenbasis-2026aAnalysisLinear AlgebraLet together with be a complex inner product space with zero vector . Let be a natural number, let be the initial segment determined by , and let be an -tuple in that is an orthonormal basis of , with comp…Action of an Operator with an Orthonormal Eigenbasis
lemmalem:orthonormal-eigenbasis-action-2026aAnalysisLinear AlgebraLet together with be a complex inner product space with zero vector . Let be a natural number, let be the initial segment determined by , and let be an -tuple in that is an orthonormal basis of , with comp…- Let be a complex vector space, let be a linear operator on , and let be a complex number. The number is an eigenvalue of if there exists a vector that is an eigenvector of with eigenvalue .
Spectral Theorem for a Self-Adjoint Operator in Finite Dimensions
theoremthm:spectral-theorem-self-adjoint-2026aAnalysisLinear AlgebraLet together with be a complex inner product space with zero vector , and suppose that is finite-dimensional and ; write for its dimension and let be the initial segment determined by . Let be a…A Self-Adjoint Operator on a Finite-Dimensional Space has a Unit Eigenvector
theoremthm:self-adjoint-eigenvalue-existence-2026aAnalysisLinear AlgebraLet together with be a complex inner product space with zero vector , and suppose that is finite-dimensional and . Let be a linear operator on that is self-adjoint. Then there are a unit vector and a…Rayleigh Quotient of a Self-Adjoint Operator
definitiondef:rayleigh-quotient-2026aAnalysisLinear AlgebraLet together with be a complex inner product space, let be a linear operator on that is self-adjoint, and let be the set of unit vectors of . The Rayleigh quotient of is the map sending each to…Elementary Properties of a Self-Adjoint Operator
lemmalem:self-adjoint-elementary-properties-2026aAnalysisLinear AlgebraLet together with be a complex inner product space with zero vector , and let be a linear operator on that is self-adjoint. Then the following hold. 1. (Real values on the diagonal) For every the complex number…- Let be a complex vector space with zero vector , let be a linear operator on , let be a complex number, and let . The vector is an eigenvector of with eigenvalue if and
The Orthogonal Complement of a Unit Vector
lemmalem:orthogonal-complement-unit-vector-2026aAnalysisLinear AlgebraLet together with be a complex inner product space with zero vector , and suppose that is finite-dimensional and ; write for its dimension. Let be a unit vector, let be the…The Orthogonal Complement of a Linear Subspace is a Linear Subspace
lemmalem:orthogonal-complement-is-subspace-2026aAnalysisLinear AlgebraLet together with be a complex inner product space and let be a linear subspace of . Then the orthogonal complement is a linear subspace of .Orthogonal Complement of a Linear Subspace
definitiondef:orthogonal-complement-2026aAnalysisLinear AlgebraLet together with be a complex inner product space and let be a linear subspace of . The orthogonal complement of is the set where is the zero…Dimension of a Finite-Dimensional Complex Inner Product Space
definitiondef:dimension-inner-product-space-2026aAnalysisLinear AlgebraLet together with be a complex inner product space with zero vector , and suppose that is finite-dimensional and . The dimension of , written , is the natural number for which there is an -tuple in t…Orthonormal Bases and Basis Size in a Finite-Dimensional Inner Product Space
lemmalem:inner-product-space-basis-size-2026aAnalysisLinear AlgebraLet together with be a complex inner product space with zero vector , and suppose that is finite-dimensional and . Then the following hold. 1. (Existence) There are a natural number and an -tuple that…- Let together with be a complex inner product space, let be a natural number, and let be an -tuple in that is linearly independent. For , with the initial segment determined by , write for the res…
A Finite Spanning Family Contains a Basis
lemmalem:spanning-family-contains-basis-2026aAlgebraLinear AlgebraLet be a field, let be a vector space over with zero vector , and suppose . Let be a natural number and let be an -tuple in that spans . Then there are a natural number with , in the order on ,…Elementary Properties of Linear Independence
lemmalem:linear-independence-elementary-2026aAlgebraLinear AlgebraLet be a field, let be a vector space over with zero vector , let be a natural number with the order relations and , and let be an -tuple in . For , with the initial segment determined by , write…A Finite Sum of Vectors with Vanishing Tail
lemmalem:finite-sum-vanishing-tail-2026aAlgebraLinear AlgebraLet be a field, let be a vector space over with zero vector , let be a natural number, let be the initial segment it determines, and let be the strict order on . Let be an -tuple in and let be such that…Any Two Orthonormal Bases of a Complex Inner Product Space Have the Same Size
theoremthm:orthonormal-basis-size-invariance-2026aAnalysisLinear AlgebraLet together with be a complex inner product space, let and be natural numbers, and let and be tuples in that are both orthonormal bases of . Then .Dropping a Redundant Vector from a Spanning Family
lemmalem:span-drop-redundant-vector-2026bAlgebraLinear AlgebraLet be a field, let be a vector space over , and let be a natural number. Inequalities between natural numbers use the order relations on . Let be a tuple in that spans , let be a natural number with , and let b…Extraction of a Summand from a Finite Sum of Vectors
lemmalem:finite-sum-extraction-2026aAlgebraLinear AlgebraLet be a field, let be a vector space over , and let be a natural number. Inequalities between natural numbers use the order relations on . Let be a tuple in , with components for , and let be a natural number wi…