How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
If has full column rank, then
Statement
Let and let have full column rank . Then is invertible and
Facts & Assumptions
Given: A matrix of full column rank, where .
Full column rank means that all singular values of are nonzero (The rank of a linear map is the number of its nonzero singular values).
Every finite real or complex matrix has a unique Moore--Penrose pseudoinverse (Every finite real or complex matrix has a unique Moore--Penrose pseudoinverse).
An invertible matrix has a two-sided inverse (Invertible matrices and the general linear group ).
Every finite real or complex matrix has a singular value decomposition (Every linear map between finite-dimensional real or complex inner product spaces admits a singular value decomposition).
Proof
By [L4], choose an SVD , and by [L1] the diagonal matrix has the form with every .
Then so [L3] gives
Multiplying by yields Direct diagonal multiplication shows that satisfies all four Penrose equations for , so uniqueness in [L2] gives .
Therefore is invertible and .
Depends on
- The rank of a linear map is the number of its nonzero singular values
- Invertible matrices and the general linear group $\operatorname{GL}_n(F)$
- Every finite real or complex matrix has a unique Moore--Penrose pseudoinverse
- Every linear map between finite-dimensional real or complex inner product spaces admits a singular value decomposition
Used by
Dependency tree · two levels
12 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Gene H. Golub, Least squares, singular values and matrix approximations (standard reference, not scraped)
- Stanford CS205L, Unit 11: Zero Singular Values (standard reference, not scraped)