theorem Matroid.isBase_of_isBase_ncard_eq_ncard {α : Type u_1} {M : Matroid α} (hM : M.RankFinite) {G I : Set α} (hGI : G.ncard = I.ncard) (hMG : M.IsBase G) (hMI : M.Indep I) : M.IsBase I

theorem Matrix.almost_square_transpose_LinearIndependent {α : Type u_1} {R : Type u_2} [Field R] {A B : Set α} [Fintype ↑A] [Fintype ↑B] (N : Matrix (↑A) (↑B) R) (hAB : #↑A = #↑B) : LinearIndependent (ι := ↑A) R N → LinearIndependent (ι := ↑B) R N.transpose

theorem StandardRepr.toMatroid.isBase_iff {α : Type u_1} {R : Type u_2} [Field R] [DecidableEq α] {S : StandardRepr α R} [Fintype ↑S.X] [Fintype ↑S.Y] {I : Set α} (hI : I ⊆ S.X ∪ S.Y) : S.toMatroid.IsBase I ↔ I.ncard = S.X.ncard ∧ LinearIndependent (ι := ↑I) R (S.toFull.submatrix id hI.elem).transpose

theorem StandardRepr.dual_toMatroid_dual {α : Type u_1} {R : Type u_2} [Field R] [DecidableEq α] (S : StandardRepr α R) [Fintype ↑S.X] [Fintype ↑S.Y] : S.toMatroid = S✶.toMatroid✶

theorem StandardRepr.dual_toMatroid {α : Type u_1} {R : Type u_2} [Field R] [DecidableEq α] (S : StandardRepr α R) [Fintype ↑S.X] [Fintype ↑S.Y] : S✶.toMatroid = S.toMatroid✶

theorem Matroid.IsRegular.dual {α : Type u_1} [DecidableEq α] {M : Matroid α} (hM : M.IsRegular) (hM_is_finite : M.Finite) : M✶.IsRegular

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