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.
Elementary row operations and row equivalence for finite matrices over a field
Definition
Let be a field and let . An elementary row operation on is one of the following operations, where row indices lie in :
- interchange two distinct rows and ;
- replace by for some nonzero ;
- replace by for distinct and some .
Matrices are row equivalent, written , when a finite sequence of elementary row operations transforms into . The empty sequence is allowed. Thus the definition also covers matrices with no rows or no columns.
Depends on
Used by
- Elementary matrices obtained by applying one elementary row operation to an identity matrix Definition
- Row swaps, arbitrary row scalings and row additions over a commutative ring, with reversible elementary cases distinguished Definition
- One matrix has two distinct row echelon forms but one reduced row echelon form Example
- Every elementary row operation has an elementary inverse, so row equivalence is an equivalence relation Lemma
- Row-equivalent matrices have the same row space and the same row rank Lemma
- Elementary row operations on an augmented matrix preserve exactly the solutions of its linear system Theorem
- Gaussian elimination reduces every finite matrix over a field to row echelon form 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 (standard reference, not scraped)