theorem neg_one_pow_mul_mem_signType_range (n : ℕ) (d : ℤ) (hd : d ∈ Set.range SignType.cast) : (-1) ^ n * d ∈ Set.range SignType.cast

theorem Matrix.det_eq_zero_of_row_combination {k : ℕ} (M : Matrix (Fin k) (Fin k) ℤ) (c : Fin k → ℤ) (hc : c ≠ 0) (hsum : ∀ (j : Fin k), ∑ i : Fin k, c i * M i j = 0) : M.det = 0

theorem Sym2.eq_mk_of_mem_of_mem {V : Type u_1} {a b : V} {e : Sym2 V} (ha : a ∈ e) (hb : b ∈ e) (hab : a ≠ b) : e = s(a, b)

theorem SimpleGraph.incMatrix_isTotallyUnimodular_of_isBipartite {V : Type u_1} [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hG : G.IsBipartite) : (incMatrix ℤ G).IsTotallyUnimodular

theorem SimpleGraph.constraintMatrix_isTotallyUnimodular_of_isBipartite {V : Type u_1} [DecidableEq V] [Fintype V] [DecidableEq (Sym2 V)] (G : SimpleGraph V) [DecidableRel G.Adj] (hG : G.IsBipartite) : ((incMatrix ℤ G).fromRows (-1)).IsTotallyUnimodular