Seymour.Results.HardDirection

source

theorem Matroid.IsRegular.isGood_of_rankFinite {α : Type u_1} [DecidableEq α] {M : Matroid α} (hM : M.IsRegular) (hM' : M.RankFinite) :

M.IsGood

The hard direction of the Seymour's theorem (restricted to matroids of finite rank).

source

theorem Matroid.RankFinite.isRegular_iff_isGood {α : Type u_1} [DecidableEq α] {M : Matroid α} (hM : M.RankFinite) :

M.IsRegular ↔ M.IsGood

Matroid of finite rank is regular iff it can be decomposed into graphic matroids & cographics matroids & matroids isomorphic to R10 using 1-sums & 2-sums & 3-sums.