Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11
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.

For equal-sized matrices, row equivalence, equality of row spaces and equality of reduced row echelon forms are equivalent

Statement

For matrices A,B∈Mm×n(F), the following are equivalent:

  1. A and B are row equivalent;
  2. Row⁡(A)=Row⁡(B);
  3. A and B have the same reduced row echelon form.

Facts & Assumptions

Given: Equal-sized matrices A and B over a field.

[L1]

Every matrix has a unique reduced row echelon form within its row-equivalence class (Every finite matrix over a field is row equivalent to exactly one reduced row echelon matrix).

[L2]

Row operations preserve row space (Row-equivalent matrices have the same row space and the same row rank).

[L3]

The nonzero rows of an echelon form form a basis of its row space (The nonzero rows of a row echelon form form a basis of the original row space).

[L4]

Every elementary row operation has an elementary inverse (Every elementary row operation has an elementary inverse, so row equivalence is an equivalence relation).

Proof

technique · direct
1.1

If A and B are row equivalent, [L2] gives equal row spaces, and reducing either one gives a reduced form in the same row-equivalence class, so [L1] gives the same RREF.

L1L2
2.1

Suppose the row spaces are the same space W. If the nonzero rows of an RREF have pivots p1<⋯<pr, then [L3] expresses every nonzero w∈W uniquely as a linear combination of those rows. The first row with nonzero coefficient makes the leading position of w equal to its pivot. Hence the pivot columns are exactly the possible leading positions of nonzero vectors in W, so both RREFs have the same pivots. Corresponding nonzero rows have 1 in the same pivot and 0 in every other pivot column. Their difference lies in W and vanishes at every possible leading position, so it is zero. The nonzero rows, and then the zero rows, agree.

step 1.1L3algebra
3.1

If A and B have a common RREF, reverse the reduction from B to that form using [L4] and concatenate it with the reduction from A; this gives a row reduction from A to B.

step 2.1L1L4∎

Depends on

Used by

Nothing in the library uses this result yet.

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