Theorem 20 — a dual has rank $n(M)$ and nullity $r(M)$

Proved

WhitneyMatroid.Duality.rank_eq_nullity_of_isDual

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

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

Let $M$ and $M'$ be matroids on finite sets of elements, with ranks $r$ and nullities $n$ , and suppose $M'$ is a dual of $M$ in the sense of (11.1). Then

r(M') = n(M),\qquad n(M') = r(M).

The rank and the nullity of the whole matroid exchange roles under duality; for a planar graph this is the exchange of the cyclomatic number and the rank of the cycle space between a graph and its dual.

Formalization Note "Dual" is IsDual, i.e. (11.1) for some one-to-one correspondence between the elements; ranks are eRk converted to integers, and all four quantities are integers.

Preamble

import Mathlib
import Definitions.Def_WhitneyMatroid_Duality_IsDual

Formal statement

namespace WhitneyMatroid.Duality

/-- Whitney, Theorem 20 (p. 522): if `M′` is a dual of `M`, then `r(M′) = n(M)` and
`n(M′) = r(M)`. -/
theorem rank_eq_nullity_of_isDual {α β : Type*} [Finite α] [Finite β] {M : Matroid α}
    {M' : Matroid β} (h : IsDual M M') :
    ((M'.eRk Set.univ).toNat : ℤ) = WhitneyMatroid.Components.nullity M Set.univ ∧
      WhitneyMatroid.Components.nullity M' Set.univ = ((M.eRk Set.univ).toNat : ℤ) := by sorry

end WhitneyMatroid.Duality

Source

Whitney, On the Abstract Properties of Linear Dependence, Amer. J. Math. 57 (1935), p. 522, Theorem 20

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

Theorem 20 — a dual has rank n(M)n(M)n(M) and nullity r(M)r(M)r(M)

Theorem 20 — a dual has rank $n(M)$ and nullity $r(M)$