feat(linear_algebra/finite_dimensional): bases given by finsets (lean…

…prover-community#3041)

In some cases, it might be more straightforward working with finsets of
the vector space instead of indexed types or carrying around a proof of
set.finite. Also provide a lemma on equal dimension
and basis cardinality lemma that uses a finset basis.

Co-authored-by: Scott Morrison scott.morrison@gmail.com

src/linear_algebra/finite_dimensional.lean

@@ -111,6 +111,19 @@ begin
   cases exists_is_basis K V with s hs,
   exact ⟨s, hs, finite_of_linear_independent hs.1⟩
 end
+
+/-- In a finite dimensional space, there exists a finite basis. Provides the basis as a finset.
+This is in contrast to `exists_is_basis_finite`, which provides a set and a `set.finite`.
+-/
+lemma exists_is_basis_finset [finite_dimensional K V] :
+  ∃ b : finset V, is_basis K (subtype.val : (↑b : set V) → V) :=
+begin
+  obtain ⟨s, s_basis, s_finite⟩ := exists_is_basis_finite K V,
+  refine ⟨s_finite.to_finset, _⟩,
+  rw set.finite.coe_to_finset,
+  exact s_basis,
+end
+
 variables {K V}
 
 /-- A vector space is finite-dimensional if and only if it is finitely generated. As the
@@ -133,6 +146,11 @@ lemma of_finite_basis {ι : Type w} [fintype ι] {b : ι → V} (h : is_basis K
   finite_dimensional K V :=
 iff_fg.2 $ ⟨finset.univ.image b, by {convert h.2, simp} ⟩
 
+/-- If a vector space has a finite basis, then it is finite-dimensional, finset style. -/
+lemma of_finset_basis {b : finset V} (h : is_basis K (subtype.val : (↑b : set V) -> V)) :
+  finite_dimensional K V :=
+iff_fg.2 $ ⟨b, by {convert h.2, simp} ⟩
+
 /-- A subspace of a finite-dimensional space is also finite-dimensional. -/
 instance finite_dimensional_submodule [finite_dimensional K V] (S : submodule K V) :
   finite_dimensional K S :=
@@ -196,6 +214,13 @@ begin
   exact (lift_inj.mp this).symm
 end
 
+/-- If a vector space has a finite basis, then its dimension is equal to the cardinality of the
+basis. This lemma uses a `finset` instead of indexed types. -/
+lemma findim_eq_card_finset_basis {b : finset V}
+  (h : is_basis K (subtype.val : (↑b : set V) -> V)) :
+  findim K V = finset.card b :=
+by { rw [findim_eq_card_basis h, fintype.subtype_card], intros x, refl }
+
 -- Note here we've restrictied the universe levels of `ι` and `V` to be the same, for convenience.
 lemma cardinal_mk_le_findim_of_linear_independent
   [finite_dimensional K V] {ι : Type v} {b : ι → V} (h : linear_independent K b) :