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

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

• graphic {α : Type} [DecidableEq α] {M : Matroid α} (hM : M.IsGraphic) : M.IsGood
• cographic {α : Type} [DecidableEq α] {M : Matroid α} (hM : M.IsCographic) : M.IsGood
• isomorphicR10 {α : Type} [DecidableEq α] {M : Matroid α} {e : α ≃ Fin 10} (hM : M.mapEquiv e = matroidR10.toMatroid) : M.IsGood
• is1sum {α : Type} [DecidableEq α] {M Mₗ Mᵣ : Matroid α} (hM : M.Is1sumOf Mₗ Mᵣ) (hMₗ : Mₗ.IsGood) (hMᵣ : Mᵣ.IsGood) : M.IsGood
• is2sum {α : Type} [DecidableEq α] {M Mₗ Mᵣ : Matroid α} (hM : M.Is2sumOf Mₗ Mᵣ) (hMₗ : Mₗ.IsGood) (hMᵣ : Mᵣ.IsGood) : M.IsGood
• is3sum {α : Type} [DecidableEq α] {M Mₗ Mᵣ : Matroid α} (hM : M.Is3sumOf Mₗ Mᵣ) (hMₗ : Mₗ.IsGood) (hMᵣ : Mᵣ.IsGood) : M.IsGood

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

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