theorem Matroid.Representable.encard_le_of_unifOn_two {α : Type u_1} {𝔽 : Type u_5} {E : Set α} [Field 𝔽] (h : (unifOn E 2).Representable 𝔽) : E.encard ≤ ENat.card 𝔽 + 1

theorem Matroid.Representable.encard_le_of_unif_two {𝔽 : Type u_5} [Field 𝔽] {a : ℕ} (h : (unif 2 a).Representable 𝔽) : ↑a ≤ ENat.card 𝔽 + 1

@[simp]

theorem Matroid.Representable.removeLoops_representable_iff {α : Type u_1} {𝔽 : Type u_5} {M : Matroid α} [Field 𝔽] : M.removeLoops.Representable 𝔽 ↔ M.Representable 𝔽

theorem Matroid.Representable.noUniformMinor {α : Type u_1} {𝔽 : Type u_5} {M : Matroid α} [Field 𝔽] [Fintype 𝔽] (h : M.Representable 𝔽) : M.NoUniformMinor 2 (Fintype.card 𝔽 + 2)

def Matroid.unifOn_rep {α : Type u_1} {𝔽 : Type u_5} [Field 𝔽] (emb : α ↪ Option 𝔽) (a : ℕ) : (unifOn Set.univ a).Rep 𝔽 (Fin a → 𝔽)

Equations

• Matroid.unifOn_rep emb a = { to_fun := Matrix.rectVandermonde (fun (i : α) => (emb i).elim 1 id) (fun (i : α) => (emb i).elim 0 1) a, indep_iff' := ⋯ }