§14 (14.1) — every real matrix has a circuit matrix

Proved

WhitneyMatroid.Fano.exists_circuitMatrix

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

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

Let $\mathbf M=(a_{ij})$ be a real $m\times n$ matrix and $M$ its matroid. For every circuit $P=\{i_1,\dots,i_p\}$ of $M$ there are real numbers $b_1,\dots,b_n$ with

a_{i1}b_1+\cdots+a_{in}b_n=0\quad(i=1,\dots,m),\qquad b_j=0\ (j\notin P),\qquad b_j\neq 0\ (j\in P). \qquad(14.1)

Consequently $\mathbf M$ has a circuit matrix: a matrix with one row for each circuit of $M$ , the row of $P$ satisfying (14.1). This makes the hypotheses of Theorems 29 and 32 and Lemmas 10 and 11 satisfiable.

Formalization Note The circuit matrix is produced with its rows indexed by the circuits of $M$ themselves (the bijection between rows and circuits is the identity).

Preamble

import Mathlib
import Definitions.Def_WhitneyMatroid_Fano_IsMatroidOf
import Definitions.Def_WhitneyMatroid_Fano_IsCircuitMatrix

Formal statement

namespace WhitneyMatroid.Fano

/-- Whitney §14, (14.1) (pp. 526–527): if `M` is the matroid of the real matrix `A`, then for every
circuit `P` of `M` there are numbers `b_1, …, b_n` with `a_{i1} b_1 + ⋯ + a_{in} b_n = 0` for all
`i`, `b_j = 0` for `j ∉ P` and `b_j ≠ 0` for `j ∈ P`; so `A` has a circuit matrix, with one row
per circuit. -/
theorem exists_circuitMatrix {ι : Type*} [Fintype ι] {m : ℕ} (A : Matrix (Fin m) ι ℝ)
    (M : Matroid ι) (hM : IsMatroidOf M A) :
    ∃ B : Matrix {P : Set ι // M.IsCircuit P} ι ℝ, IsCircuitMatrix M A B (Equiv.refl _) := by sorry

end WhitneyMatroid.Fano

Source

Whitney, On the Abstract Properties of Linear Dependence, Amer. J. Math. 57 (1935), pp. 526–527, §14, (14.1)

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