Alphabeta Math
LemmaStatement: 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.

Elementary row operations preserve every linear relation among the columns and hence preserve column rank

Statement

If B is row equivalent to A, then for every coefficient column c, Ac=0⟺Bc=0. Thus row operations preserve all linear relations among corresponding columns, preserve which column subfamilies are linearly independent, and preserve column rank.

Facts & Assumptions

Given: Row-equivalent matrices A,B∈Mm×n(F) and c∈Fn.

[L1]

Row operations on an augmented matrix preserve its solution set (Elementary row operations on an augmented matrix preserve exactly the solutions of its linear system).

[L2]

Column space is the span of the columns and column rank is its dimension (Row space, column space, nullspace, row rank, column rank and matrix rank).

Proof

technique · direct
1.1

The equation Ac=0 says exactly that the columns of A, with coefficients cj, have zero linear combination.

L2L3
2.1

Apply the same row operations to [A∣0]. Its last column stays zero, so [L1] gives Ac=0 if and only if Bc=0.

step 1.1L1
3.1

Restricting c to any chosen column subfamily shows that it is independent for A exactly when it is independent for B. Hence the largest independent column families and their dimension agree, although the literal column spaces may differ.

step 2.1L2L3∎

Depends on

Used by

Dependency tree · two levels

18 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