def matroidR10 {α : Type} [DecidableEq α] : StandardRepr α Z2

TODO define R10.

Equations

• matroidR10 = sorry

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
• theR10 {α : 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₂) : M.IsGood
• is2sum {α : Type} [DecidableEq α] {M M₁ M₂ : Matroid α} (hM : M.Is2sumOf M₁ M₂) : M.IsGood
• is3sum {α : Type} [DecidableEq α] {M M₁ M₂ : Matroid α} (hM : M.Is3sumOf M₁ M₂) : M.IsGood

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

THE HOLY GRAIL.