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.
Row echelon form, reduced row echelon form, leading entries, pivots, pivot positions and pivot columns
Definition
In a nonzero row of a matrix over a field, its leading entry is its leftmost nonzero entry. A matrix is in row echelon form when:
- every zero row lies below every nonzero row;
- the leading entry of each nonzero row lies strictly to the right of the leading entry in the row above it;
- every entry below a leading entry is zero.
A leading entry in row echelon form is a pivot. Its location is a pivot position, and a column containing a pivot is a pivot column.
A row echelon matrix is in reduced row echelon form when every pivot equals and is the only nonzero entry in its column. Zero-row, zero-column and all-zero matrices satisfy these conditions vacuously.
Depends on
Used by
- One matrix has two distinct row echelon forms but one reduced row echelon form Example
- The nonzero rows of a row echelon form form a basis of the original row space Lemma
- A finite square real matrix is invertible if and only if its determinant is nonzero Theorem
- Every finite matrix over a field is row equivalent to exactly one reduced row echelon matrix Theorem
- Gauss–Jordan elimination reduces every finite matrix over a field to reduced row echelon form Theorem
- Gaussian elimination reduces every finite matrix over a field to row echelon form Theorem
- Reduced row echelon form detects consistency and parametrises every solution by the nonpivot variables Theorem
- The columns of the original matrix indexed by pivot columns form a basis of its column space Theorem
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 26 results over 10 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, §§1.2–1.3 (standard reference, not scraped)
- J. Hefferon, Linear Algebra, 4th ed., Ch. One, §III.1 (standard reference, not scraped)