Row equivalence is sameness of row space

Proved

HefferonLinAlg.row_equivalent_iff_same_row_space

by tianyipeng · Aug 5, 2026 · Mathlib c5ea003 (Lean v4.30.0)

echelon-formlinear-algebrarow-space

Two $m \times n$ matrices $A$ and $B$ over a field $K$ are row equivalent — that is, $B = MA$ for some invertible $M$ — if and only if the span of the rows of $A$ equals the span of the rows of $B$ . This is where Chapter One's Linear Combination Lemma arrives: row reduction changes the rows but never the subspace they span, and that invariant is complete, which is what makes reduced echelon form a genuine canonical form for row equivalence.

Preamble

import Mathlib

open Matrix

Formal statement

namespace HefferonLinAlg

theorem row_equivalent_iff_same_row_space
    {K : Type*} [Field K] {m n : ℕ} (A B : Matrix (Fin m) (Fin n) K) :
    (∃ M : Matrix (Fin m) (Fin m) K, IsUnit M.det ∧ B = M * A) ↔
      Submodule.span K (Set.range A) = Submodule.span K (Set.range B) := by
  sorry

end HefferonLinAlg

Source

Jim Hefferon, *Linear Algebra*, Saint Michael's College, 2020 printing, Chapter One, Section III.2 and Chapter Two, Section III.3, Lemma 3.5 / Theorem 3.7, pp. 66-74, 146-153

Read-back

What the Lean code literally says, in plain math · claude-opus-5

For every field $K$ (an arbitrary type carrying a field structure), every pair of natural numbers $m, n$ (both allowed to be $0$ ), and every two matrices $A, B$ of the same shape $m \times n$ with entries in $K$ — indexed by $\{0,\dots,m-1\} \times \{0,\dots,n-1\}$ — the following two statements are asserted to be equivalent (a genuine two-directional "if and only if", not an implication in one direction):

\Big(\exists\, M \in K^{m \times m} : \det M \text{ is a unit of } K \ \text{ and } \ B = M A\Big) \quad\Longleftrightarrow\quad \operatorname{span}_K\big(\mathcal{R}(A)\big) \;=\; \operatorname{span}_K\big(\mathcal{R}(B)\big).

Here the left-hand side quantifies existentially over square matrices $M$ of size $m \times m$ over the same field, requires that $\det M$ be an invertible element of $K$ (over a field this is exactly $\det M \neq 0$ ; note that for $m = 0$ the determinant of the unique empty matrix is $1$ , which is a unit, so the condition is satisfiable there), and requires the exact matrix identity $B = M A$ with $M$ multiplied on the left of $A$ (ordinary matrix product, so each row of $B$ is the corresponding $K$ -linear combination of the rows of $A$ with coefficients from that row of $M$ ); no condition whatsoever is imposed on $A$ or $B$ themselves (they may be zero, may be equal, may have repeated rows). On the right-hand side, for a matrix $X$ of shape $m \times n$ the set $\mathcal{R}(X)$ is literally the range of $X$ viewed as a function of its first index, i.e. the set of its rows

\mathcal{R}(X) \;=\; \{\, X_{i,\bullet} \;:\; i \in \{0,\dots,m-1\} \,\} \;\subseteq\; K^{n},

a subset of the $K$ -vector space $K^{n}$ of functions from $\{0,\dots,n-1\}$ to $K$ — a set, so repeated rows are counted once and no multiplicity or ordering information is retained — and $\operatorname{span}_K(\cdot)$ is the smallest $K$ -linear subspace of $K^{n}$ containing that set; the asserted relation between the two spans is equality of subspaces (mutual inclusion), not merely one inclusion. Degenerate cases are included silently by the quantifiers: when $m = 0$ both row sets are empty and both spans are the zero subspace, and the unique $0 \times 0$ matrix $M$ has unit determinant, so both sides hold; when $n = 0$ the space $K^{0}$ is the zero space, every row is the zero vector, both spans are again the zero subspace, and the identity matrix witnesses the left side, so both sides hold as well. The statement says nothing about uniqueness of $M$ , nothing about $A$ and $B$ having any particular rank, and nothing about column spaces or about matrices of differing row counts.

Human review

Endorsed by Shuze Chen · Aug 5, 2026
Endorsed by tianyipeng · Aug 5, 2026
Confirmed by the mission captain (proposal self-audit).

View graph