[Merged by Bors] - feat(linear_algebra/finite_dimensional): bases given by finsets

src/linear_algebra/finite_dimensional.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2019 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Chris Hughes
+Authors: Chris Hughes, Yakov Pechersky
 -/
 import linear_algebra.dimension
 import ring_theory.principal_ideal_domain
@@ -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 finite_dimensional.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⟩ := finite_dimensional.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_finite_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 is finite-dimensional, then the cardinality of any basis is equal to its
+`findim`. This lemma uses finsets instead of indexed types. -/
+lemma finite_dimensional.findim_eq_card_basis'' [finite_dimensional K V] {b : finset V}
+  (h : is_basis K (subtype.val : (↑b : set V) -> V)) :
+  findim K V = finset.card b :=
+by { rw [finite_dimensional.findim_eq_card_basis h, fintype.subtype_card], intros x, refl }
+
 /-- If a submodule has maximal dimension in a finite dimensional space, then it is equal to the
 whole space. -/
 lemma eq_top_of_findim_eq [finite_dimensional K V] {S : submodule K V}