@[simp]

theorem ne_one_iff {x : ZMod 2} : x ≠ 1 ↔ x = 0

@[simp]

theorem ne_zero_iff {x : ZMod 2} : x ≠ 0 ↔ x = 1

theorem Matroid.Rep.cyclic_of_forall_row_even {α : Type u_1} {ι : Type u_7} {M : Matroid α} {C : Finset α} (v : M.Rep (ZMod 2) (ι →₀ ZMod 2)) (hCE : ↑C ⊆ M.E) (h_even : ∀ (i : ι), Even {x ∈ C | (v x) i = 1}.card) : M.Cyclic ↑C

If every row of the submatrix induced by C has even support, then C is cyclic.

theorem Matroid.Rep.row_even_of_isCircuit {α : Type u_1} {ι : Type u_7} {M : Matroid α} (v : M.Rep (ZMod 2) (ι →₀ ZMod 2)) {C : Finset α} (hC : M.IsCircuit ↑C) (i : ι) : Even {x ∈ C | (v x) i = 1}.card

If C is a circuit, then every row of the corresponding submatrix has even support.

noncomputable def Matroid.IsBase.BinaryProxy {α : Type u_1} {B : Set α} {M : Matroid α} [M.Finitary] (hB : M.IsBase B) : Matroid α

The Binary matroid that should be M, with representation given by the fundamental matrix of a base B. If M is binary, this is equal to M.

Equations

• hB.BinaryProxy = Matroid.ofFun (ZMod 2) M.E (hB.fundCoord (ZMod 2))

noncomputable def Matroid.IsBase.binaryProxyRep {α : Type u_1} {B : Set α} {M : Matroid α} [M.Finitary] (hB : M.IsBase B) : hB.BinaryProxy.Rep (ZMod 2) (↑B →₀ ZMod 2)

Equations

• hB.binaryProxyRep = Matroid.repOfFun (ZMod 2) M.E (hB.fundCoord (ZMod 2))

instance Matroid.instFinitaryBinaryProxy {α : Type u_1} {B : Set α} {M : Matroid α} [M.Finitary] {hB : M.IsBase B} : hB.BinaryProxy.Finitary

theorem Matroid.IsBase.binaryProxyRep_isStandard {α : Type u_1} {B : Set α} {M : Matroid α} [M.Finitary] (hB : M.IsBase B) : hB.binaryProxyRep.IsStandard

theorem Matroid.CrossingBinary.eq_binaryProxy {α : Type u_1} {B : Set α} {M : Matroid α} [M.Finitary] (hM : M.CrossingBinary) (hB : M.IsBase B) : M = hB.BinaryProxy

theorem Matroid.representable_iff_no_U24_isMinor {α : Type u_1} {M : Matroid α} [M.Finitary] : M.Representable (ZMod 2) ↔ M.NoUniformMinor 2 4

Tutte's excluded minor characterization of the binary matroids : A matroid has a GF(2)-representation iff it has no U₂,₄-minor. This version applies to all finitary matroids.

theorem Matroid.crossingBinary_iff_representable {α : Type u_1} {M : Matroid α} [M.Finitary] : M.CrossingBinary ↔ M.Representable (ZMod 2)