Alphabeta MathHow 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.
Every invertible finite square real matrix is a finite product of elementary matrices
Statement
Every invertible matrix is a finite product of elementary matrices. The identity matrix is represented by the empty product.
Facts & Assumptions
Given: An invertible real matrix .
An invertible matrix has RREF (Invertible matrix theorem: invertibility, full pivot rank, RREF , trivial nullspace and unique solvability are equivalent).
A row reduction is left multiplication by a product of its elementary matrices (A finite row reduction from to is encoded by ).
The inverse of an elementary matrix is elementary (Every elementary matrix is invertible, with inverse given by the reverse elementary operation).
The real numbers form a field (The reals form a field).
Proof
By [L1] row reduction takes to ; by [L2] there are elementary real matrices with .
Multiply by the explicit inverses in reverse order to obtain , and each factor is elementary by [L3].
If , take and the empty product. No determinant is used.
Depends on
- Invertible matrix theorem: invertibility, full pivot rank, RREF $I$, trivial nullspace and unique solvability are equivalent
- A finite row reduction from $A$ to $B$ is encoded by $B=E_r\cdots E_1A$
- Every elementary matrix is invertible, with inverse given by the reverse elementary operation
- The reals form a field
Used by
- An invertible 3×3 real matrix factored explicitly into elementary matrices Example
- Smooth orientation sign is the local integral homology multiplier Lemma
- A linear endomorphism of ℝⁿ sends bounded Jordan sets to bounded Jordan sets and scales their content by the absolute determinant Theorem
- A linear map T of ℝⁿ sends Lebesgue measurable sets to Lebesgue measurable sets, with λₙ(T[E])=|det T| λₙ(E) when T is invertible and T[E] Lebesgue null when it is not Theorem
Dependency tree · two levels
21 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
- J. Hefferon, Linear Algebra, 4th ed., Ch. Three, §IV.3 (standard reference, not scraped)