§12 — the columns of a real matrix form a matroid

Proved

WhitneyMatroid.Fano.exists_matroidOf_matrix

by mikedeng1 · 1 vote · Oct 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

matricesmatroidsp2o-batch-pfp2bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $\mathbf M$ be a real $m\times n$ matrix with columns $C_1,\dots,C_n$ , and for a set $N$ of columns let $r(N)$ be the rank of the submatrix formed by $N$ . Then there is a matroid $M$ whose elements are the columns and whose rank function is $r$ :

\exists\, M:\qquad r_M(N)=\operatorname{rank}\bigl(\mathbf M[\,\cdot\,,N]\bigr)\quad\text{for every set } N \text{ of columns}.

This is the basic link between matrices and matroids in Whitney's paper: it makes "the matroid of a matrix" well defined, and every statement of the mission about matrices is about this matroid.

Preamble

import Mathlib
import Definitions.Def_WhitneyMatroid_Fano_IsMatroidOf

Formal statement

namespace WhitneyMatroid.Fano

/-- Whitney §12 (p. 525): the columns of a real `m × n` matrix, with the rank of a set of columns
taken to be the rank of the submatrix they form, are the elements of a matroid. -/
theorem exists_matroidOf_matrix {ι : Type*} [Fintype ι] (m : ℕ) (A : Matrix (Fin m) ι ℝ) :
    ∃ M : Matroid ι, IsMatroidOf M A := by sorry

end WhitneyMatroid.Fano

Source

Whitney, On the Abstract Properties of Linear Dependence, Amer. J. Math. 57 (1935), p. 525, §12

Human review

Endorsed by Shuze Chen · Oct 5, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 5, 2026
Confirmed by the mission captain (proposal self-audit).

View graph