inductive Matroid.IsGood {α : Type u_1} [DecidableEq α] : Matroid α → Prop

Given matroid can be constructed from graphic matroids & cographics matroids & R10 using 1-sums & 2-sums & 3-sums.

• graphic {α : Type u_1} [DecidableEq α] {M : Matroid α} (hM : M.IsGraphic) : M.IsGood
• cographic {α : Type u_1} [DecidableEq α] {M : Matroid α} (hM : M.IsCographic) : M.IsGood
• isomorphicR10 {α : Type u_1} [DecidableEq α] {M : Matroid α} {e : α ≃ Fin 10} (hM : M.mapEquiv e = matroidR10.toMatroid) : M.IsGood
• is1sum {α : Type u_1} [DecidableEq α] {M Mₗ Mᵣ : Matroid α} (hMMM : M.IsSum1of Mₗ Mᵣ) (hM : M.RankFinite) (hMₗ : Mₗ.IsGood) (hMᵣ : Mᵣ.IsGood) : M.IsGood
• is2sum {α : Type u_1} [DecidableEq α] {M Mₗ Mᵣ : Matroid α} (hMMM : M.IsSum2of Mₗ Mᵣ) (hM : M.RankFinite) (hMₗ : Mₗ.IsGood) (hMᵣ : Mᵣ.IsGood) : M.IsGood
• is3sum {α : Type u_1} [DecidableEq α] {M Mₗ Mᵣ : Matroid α} (hMMM : M.IsSum3of Mₗ Mᵣ) (hM : M.RankFinite) (hMₗ : Mₗ.IsGood) (hMᵣ : Mᵣ.IsGood) : M.IsGood

theorem Matroid.IsGood.isRegular {α : Type u_1} [DecidableEq α] {M : Matroid α} (hM : M.IsGood) : M.IsRegular

Corollary of the easy direction of the Seymour's theorem.

theorem Matroid.IsGood.isBinary {α : Type u_1} [DecidableEq α] {M : Matroid α} (hM : M.IsGood) : ∃ (X : Set α) (Y : Set α) (A : Matrix (↑X) (↑Y) Z2), A.toMatroid = M

Every good matroid is binary.