theorem LinearIndepOn.encard_le_toENat_rank' {ι : Type u_1} {R : Type u_2} {M : Type u_3} [Semiring R] [Nontrivial R] [AddCommMonoid M] [Module R M] {s : Set ι} {v : ι → M} (hs : LinearIndepOn R v s) : s.encard ≤ Cardinal.toENat (Module.rank R M)

theorem rectVandermonde_rows_linearIndependent {n : ℕ} {α : Type u_3} {R : Type u_4} [CommRing R] [IsDomain R] [Fintype α] (hcard : Fintype.card α ≤ n) {v w : α → R} (hvw : ∀ ⦃i i' : α⦄, v i * w i' = v i' * w i → i = i') (h0 : ∀ ⦃i : α⦄, w i = 0 → v i ≠ 0) : LinearIndependent R (Matrix.rectVandermonde v w n)

If v i and w i are never both zero, and v i * w i' ≠ v i' * w i for all i ≠ i', and the rectangular Vandermonde matrix coming from v and w has at least as many columns as rows, then its rows are linearly independent.

theorem rectVandermonde_linearIndepOn_iff {n : ℕ} {α : Type u_3} {R : Type u_4} [CommRing R] [IsDomain R] {v w : α → R} {s : Set α} (hn : n ≠ 1) : LinearIndepOn R (Matrix.rectVandermonde v w n) s ↔ s.encard ≤ ↑n ∧ (∀ i ∈ s, v i = 0 → w i ≠ 0) ∧ ∀ ⦃i j : α⦄, i ∈ s → j ∈ s → v j * w i = v i * w j → i = j

A set s of rows of rectVandermonde v w n is linearly independent if and only if its cardinality doesn't exceed the number of columns, there is no co-ordinate in s on which both v i and w i are zero, and v i * w j ≠ v j * w i for distinct i,j ∈ s. (We require n = 1, since otherwise v i = w i = 0 and s.encard = 1 gives a counterexample.)

theorem rectVandermonde_linearIndepOn_iff₀ {n : ℕ} {α : Type u_3} {R : Type u_4} [CommRing R] [IsDomain R] {v w : α → R} {s : Set α} (hvw : ∀ i ∈ s, v i = 0 → w i ≠ 0) : LinearIndepOn R (fun (i : α) => Matrix.rectVandermonde v w n i) s ↔ s.encard ≤ ↑n ∧ ∀ ⦃i j : α⦄, i ∈ s → j ∈ s → v j * w i = v i * w j → i = j

theorem rectVandermonde_one_linearIndepOn_iff {n : ℕ} {K : Type u_2} [Field K] {α : Type u_3} {v : α → K} {s : Set α} : LinearIndepOn K (fun (i : α) => Matrix.rectVandermonde v 1 n i) s ↔ s.encard ≤ ↑n ∧ Set.InjOn v s

A version of rectVandermonde_linearIndepOn_iff for the 'non-projective' Vandermonde matrix with rows of the form [1,x,...,x^(n-1)]. In this case, linear independence is just injectivity.