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.
The columns of the original matrix indexed by pivot columns form a basis of its column space
Statement
Let be the reduced row echelon form of . The columns of whose indices are pivot columns of form a basis of .
Facts & Assumptions
Given: A matrix and its RREF .
Row operations preserve every linear relation among corresponding columns (Elementary row operations preserve every linear relation among the columns and hence preserve column rank).
A pivot column of an RREF is a unit column, and every nonpivot column has entries only in the pivot rows (Row echelon form, reduced row echelon form, leading entries, pivots, pivot positions and pivot columns).
The column space is the span of all columns (Row space, column space, nullspace, row rank, column rank and matrix rank).
A basis is a linearly independent spanning family (Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis).
Proof
In , the pivot columns are distinct unit columns, so they are independent. Every nonpivot column equals the linear combination of those unit columns whose coefficients are its entries in the pivot rows, so the pivot columns span every column of .
Each relation used in step 1.1 holds among the corresponding columns of by [L1], and every relation among the pivot columns transfers in both directions.
Therefore the original pivot-indexed columns are independent and span every column of , hence form a basis of .
Depends on
- Elementary row operations preserve every linear relation among the columns and hence preserve column rank
- Row echelon form, reduced row echelon form, leading entries, pivots, pivot positions and pivot columns
- Row space, column space, nullspace, row rank, column rank and matrix rank
- Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 63 results over 21 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- D. Margalit and J. Rabinoff, Interactive Linear Algebra, §3.5 (standard reference, not scraped)