diff --git a/src/analysis/normed_space/finite_dimension.lean b/src/analysis/normed_space/finite_dimension.lean
index bf5c81275a5ec..601d123000db6 100644
--- a/src/analysis/normed_space/finite_dimension.lean
+++ b/src/analysis/normed_space/finite_dimension.lean
@@ -112,7 +112,7 @@ begin
         { left,
           have : finrank 𝕜 f.range = 1,
           { refine le_antisymm _ (zero_lt_iff.mpr H),
-            simpa [finrank_of_field] using f.range.finrank_le },
+            simpa [finrank_self] using f.range.finrank_le },
           rw [this, add_comm, nat.add_one] at Z,
           exact nat.succ.inj Z } },
       have : is_closed (f.ker : set E),
diff --git a/src/field_theory/finite/polynomial.lean b/src/field_theory/finite/polynomial.lean
index e27a22fd2d938..0e3373f8cd5da 100644
--- a/src/field_theory/finite/polynomial.lean
+++ b/src/field_theory/finite/polynomial.lean
@@ -159,7 +159,7 @@ calc module.rank K (R σ K) =
     linear_equiv.dim_eq
       (finsupp.supported_equiv_finsupp {s : σ →₀ ℕ | ∀n:σ, s n ≤ fintype.card K - 1 })
   ... = cardinal.mk {s : σ →₀ ℕ | ∀ (n : σ), s n ≤ fintype.card K - 1} :
-    by rw [finsupp.dim_eq, dim_of_ring, mul_one]
+    by rw [finsupp.dim_eq, dim_self, mul_one]
   ... = cardinal.mk {s : σ → ℕ | ∀ (n : σ), s n < fintype.card K } :
   begin
     refine quotient.sound ⟨equiv.subtype_equiv finsupp.equiv_fun_on_fintype $ assume f, _⟩,
diff --git a/src/linear_algebra/dimension.lean b/src/linear_algebra/dimension.lean
index b9798e18b53cf..8ec3395d7bb8f 100644
--- a/src/linear_algebra/dimension.lean
+++ b/src/linear_algebra/dimension.lean
@@ -227,6 +227,10 @@ begin
   apply dim_range_le,
 end
 
+theorem dim_quotient_le (p : submodule R M) :
+  module.rank R p.quotient ≤ module.rank R M :=
+(mkq p).dim_le_of_surjective (surjective_quot_mk _)
+
 variables [nontrivial R]
 
 lemma {m} cardinal_lift_le_dim_of_linear_independent
@@ -717,6 +721,13 @@ theorem basis.mk_range_eq_dim (v : basis ι R M) :
   cardinal.mk (range v) = module.rank R M :=
 v.reindex_range.mk_eq_dim''
 
+/-- If a vector space has a finite basis, then its dimension (seen as a cardinal) is equal to the
+cardinality of the basis. -/
+lemma dim_eq_card_basis {ι : Type w} [fintype ι] (h : basis ι R M) :
+  module.rank R M = fintype.card ι :=
+by rw [←h.mk_range_eq_dim, cardinal.fintype_card,
+       set.card_range_of_injective h.injective]
+
 theorem basis.mk_eq_dim (v : basis ι R M) :
   cardinal.lift.{w v} (cardinal.mk ι) = cardinal.lift.{v w} (module.rank R M) :=
 by rw [←v.mk_range_eq_dim, cardinal.mk_range_eq_of_injective v.injective]
@@ -757,7 +768,7 @@ by { rw [← @set_of_mem_eq _ s, ← subtype.range_coe_subtype], exact dim_span
 
 variables (R)
 
-lemma dim_of_ring : module.rank R R = 1 :=
+lemma dim_self : module.rank R R = 1 :=
 by rw [←cardinal.lift_inj, ← (basis.singleton punit R).mk_eq_dim, cardinal.mk_punit]
 
 end strong_rank_condition
@@ -852,6 +863,68 @@ begin
       ⟨equiv.ulift.trans (equiv.sum_congr equiv.ulift equiv.ulift).symm ⟩),
 end
 
+-- TODO the remainder of this section should generalize beyond division rings.
+
+lemma dim_zero_iff_forall_zero : module.rank K V = 0 ↔ ∀ x : V, x = 0 :=
+begin
+  split,
+  { intros h x,
+    have card_mk_range := (basis.of_vector_space K V).mk_range_eq_dim,
+    rw [h, cardinal.mk_emptyc_iff, coe_of_vector_space, subtype.range_coe] at card_mk_range,
+    simpa [card_mk_range] using (of_vector_space K V).mem_span x },
+  { intro h,
+    have : (⊤ : submodule K V) = ⊥,
+    { ext x, simp [h x] },
+    rw [←dim_top, this, dim_bot] }
+end
+
+lemma dim_zero_iff : module.rank K V = 0 ↔ subsingleton V :=
+dim_zero_iff_forall_zero.trans (subsingleton_iff_forall_eq 0).symm
+
+lemma dim_pos_iff_exists_ne_zero : 0 < module.rank K V ↔ ∃ x : V, x ≠ 0 :=
+begin
+  rw ←not_iff_not,
+  simpa using dim_zero_iff_forall_zero
+end
+
+lemma dim_pos_iff_nontrivial : 0 < module.rank K V ↔ nontrivial V :=
+dim_pos_iff_exists_ne_zero.trans (nontrivial_iff_exists_ne 0).symm
+
+lemma dim_pos [h : nontrivial V] : 0 < module.rank K V :=
+dim_pos_iff_nontrivial.2 h
+
+
+section fintype
+variable [fintype η]
+variables [∀i, add_comm_group (φ i)] [∀i, module K (φ i)]
+
+open linear_map
+
+lemma dim_pi : module.rank K (Πi, φ i) = cardinal.sum (λi, module.rank K (φ i)) :=
+begin
+  let b := assume i, basis.of_vector_space K (φ i),
+  let this : basis (Σ j, _) K (Π j, φ j) := pi.basis b,
+  rw [←cardinal.lift_inj, ← this.mk_eq_dim],
+  simp [λ i, (b i).mk_range_eq_dim.symm, cardinal.sum_mk]
+end
+
+lemma dim_fun {V η : Type u} [fintype η] [add_comm_group V] [module K V] :
+  module.rank K (η → V) = fintype.card η * module.rank K V :=
+by rw [dim_pi, cardinal.sum_const, cardinal.fintype_card]
+
+lemma dim_fun_eq_lift_mul :
+  module.rank K (η → V) = (fintype.card η : cardinal.{max u₁' v}) *
+    cardinal.lift.{v u₁'} (module.rank K V) :=
+by rw [dim_pi, cardinal.sum_const_eq_lift_mul, cardinal.fintype_card, cardinal.lift_nat_cast]
+
+lemma dim_fun' : module.rank K (η → K) = fintype.card η :=
+by rw [dim_fun_eq_lift_mul, dim_self, cardinal.lift_one, mul_one, cardinal.nat_cast_inj]
+
+lemma dim_fin_fun (n : ℕ) : module.rank K (fin n → K) = n :=
+by simp [dim_fun']
+
+end fintype
+
 end division_ring
 
 section field
@@ -863,10 +936,6 @@ theorem dim_quotient_add_dim (p : submodule K V) :
   module.rank K p.quotient + module.rank K p = module.rank K V :=
 by classical; exact let ⟨f⟩ := quotient_prod_linear_equiv p in dim_prod.symm.trans f.dim_eq
 
-theorem dim_quotient_le (p : submodule K V) :
-  module.rank K p.quotient ≤ module.rank K V :=
-by { rw ← dim_quotient_add_dim p, exact self_le_add_right _ _ }
-
 /-- rank-nullity theorem -/
 theorem dim_range_add_dim_ker (f : V →ₗ[K] V₁) :
   module.rank K f.range + module.rank K f.ker = module.rank K V :=
@@ -944,37 +1013,6 @@ by { rw [← dim_sup_add_dim_inf_eq], exact self_le_add_right _ _ }
 
 end
 
-section fintype
-variable [fintype η]
-variables [∀i, add_comm_group (φ i)] [∀i, module K (φ i)]
-
-open linear_map
-
-lemma dim_pi : module.rank K (Πi, φ i) = cardinal.sum (λi, module.rank K (φ i)) :=
-begin
-  let b := assume i, basis.of_vector_space K (φ i),
-  let this : basis (Σ j, _) K (Π j, φ j) := pi.basis b,
-  rw [←cardinal.lift_inj, ← this.mk_eq_dim],
-  simp [λ i, (b i).mk_range_eq_dim.symm, cardinal.sum_mk]
-end
-
-lemma dim_fun {V η : Type u} [fintype η] [add_comm_group V] [module K V] :
-  module.rank K (η → V) = fintype.card η * module.rank K V :=
-by rw [dim_pi, cardinal.sum_const, cardinal.fintype_card]
-
-lemma dim_fun_eq_lift_mul :
-  module.rank K (η → V) = (fintype.card η : cardinal.{max u₁' v}) *
-    cardinal.lift.{v u₁'} (module.rank K V) :=
-by rw [dim_pi, cardinal.sum_const_eq_lift_mul, cardinal.fintype_card, cardinal.lift_nat_cast]
-
-lemma dim_fun' : module.rank K (η → K) = fintype.card η :=
-by rw [dim_fun_eq_lift_mul, dim_of_ring, cardinal.lift_one, mul_one, cardinal.nat_cast_inj]
-
-lemma dim_fin_fun (n : ℕ) : module.rank K (fin n → K) = n :=
-by simp [dim_fun']
-
-end fintype
-
 lemma exists_mem_ne_zero_of_ne_bot {s : submodule K V} (h : s ≠ ⊥) : ∃ b : V, b ∈ s ∧ b ≠ 0 :=
 begin
   classical,
@@ -1035,21 +1073,6 @@ end rank
 
 -- TODO The remainder of this file could be generalized to arbitrary rings.
 
-lemma dim_zero_iff_forall_zero : module.rank K V = 0 ↔ ∀ x : V, x = 0 :=
-begin
-  split,
-  { intros h x,
-    have card_mk_range := (basis.of_vector_space K V).mk_range_eq_dim,
-    rw [h, cardinal.mk_emptyc_iff, coe_of_vector_space, subtype.range_coe] at card_mk_range,
-    simpa [card_mk_range] using (of_vector_space K V).mem_span x },
-  { intro h,
-    have : (⊤ : submodule K V) = ⊥,
-    { ext x, simp [h x] },
-    rw [←dim_top, this, dim_bot] }
-end
-
-lemma dim_zero_iff : module.rank K V = 0 ↔ subsingleton V :=
-dim_zero_iff_forall_zero.trans (subsingleton_iff_forall_eq 0).symm
 
 /-- The `ι` indexed basis on `V`, where `ι` is an empty type and `V` is zero-dimensional.
 
@@ -1067,19 +1090,6 @@ end
   basis.of_dim_eq_zero hV i = 0 :=
 rfl
 
-
-lemma dim_pos_iff_exists_ne_zero : 0 < module.rank K V ↔ ∃ x : V, x ≠ 0 :=
-begin
-  rw ←not_iff_not,
-  simpa using dim_zero_iff_forall_zero
-end
-
-lemma dim_pos_iff_nontrivial : 0 < module.rank K V ↔ nontrivial V :=
-dim_pos_iff_exists_ne_zero.trans (nontrivial_iff_exists_ne 0).symm
-
-lemma dim_pos [h : nontrivial V] : 0 < module.rank K V :=
-dim_pos_iff_nontrivial.2 h
-
 lemma le_dim_iff_exists_linear_independent {c : cardinal} :
   c ≤ module.rank K V ↔ ∃ s : set V, cardinal.mk s = c ∧ linear_independent K (coe : s → V) :=
 begin
diff --git a/src/linear_algebra/finite_dimensional.lean b/src/linear_algebra/finite_dimensional.lean
index 7cc3791e11df4..cec762ebcf69e 100644
--- a/src/linear_algebra/finite_dimensional.lean
+++ b/src/linear_algebra/finite_dimensional.lean
@@ -66,6 +66,9 @@ and the equivalence between left-inverse and right-inverse in `mul_eq_one_comm`
 Most results are deduced from the corresponding results for the general dimension (as a cardinal),
 in `dimension.lean`. Not all results have been ported yet.
 
+Much of this file could be generalised away from fields or division rings.
+You should not assume that there has been any effort to state lemmas as generally as possible.
+
 One of the characterizations of finite-dimensionality is in terms of finite generation. This
 property is currently defined only for submodules, so we express it through the fact that the
 maximal submodule (which, as a set, coincides with the whole space) is finitely generated. This is
@@ -80,21 +83,28 @@ open_locale classical
 
 open cardinal submodule module function
 
-variables {K : Type u} {V : Type v} [field K] [add_comm_group V] [module K V]
-variables {V₂ : Type v'} [add_comm_group V₂] [module K V₂]
-
 /-- `finite_dimensional` vector spaces are defined to be noetherian modules.
 Use `finite_dimensional.iff_fg` or `finite_dimensional.of_fintype_basis` to prove finite dimension
 from a conventional definition. -/
-@[reducible] def finite_dimensional (K V : Type*) [field K]
+@[reducible] def finite_dimensional (K V : Type*) [division_ring K]
   [add_comm_group V] [module K V] := is_noetherian K V
 
 namespace finite_dimensional
 
 open is_noetherian
 
+section division_ring
+
+variables (K : Type u) (V : Type v) [division_ring K] [add_comm_group V] [module K V]
+{V₂ : Type v'} [add_comm_group V₂] [module K V₂]
+
 variables (K V)
 
+-- Without this apparently redundant instance we get typeclass search errors
+-- in `analysis.normed_space.finite_dimension`.
+instance finite_dimensional_pi {ι} [fintype ι] : finite_dimensional K (ι → K) :=
+is_noetherian_pi
+
 /-- A finite dimensional vector space over a finite field is finite -/
 noncomputable def fintype_of_fintype [fintype K] [is_noetherian K V] : fintype V :=
 module.fintype_of_fintype (finset_basis K V)
@@ -112,9 +122,8 @@ lemma of_finite_basis {ι : Type w} {s : set ι} (h : basis s K V) (hs : set.fin
   finite_dimensional K V :=
 by haveI := hs.fintype; exact of_fintype_basis h
 
--- TODO: why do we have to specify `.{w}` explicitly here?
 /-- If a vector space has a finite basis, then it is finite-dimensional, finset style. -/
-lemma of_finset_basis {ι : Type w} {s : finset ι} (h : basis.{w} s K V) :
+lemma of_finset_basis {ι : Type w} {s : finset ι} (h : basis s K V) :
   finite_dimensional K V :=
 of_finite_basis h s.finite_to_set
 
@@ -135,13 +144,13 @@ Defined by convention to be `0` if the space has infinite rank.
 For a vector space `V` over a field `K`, this is the same as the finite dimension
 of `V` over `K`.
 -/
-noncomputable def finrank (K V : Type*) [field K]
+noncomputable def finrank (K V : Type*) [division_ring K]
   [add_comm_group V] [module K V] : ℕ :=
 (module.rank K V).to_nat
 
 /-- In a finite-dimensional space, its dimension (seen as a cardinal) coincides with its
 `finrank`. -/
-lemma finrank_eq_dim (K : Type u) (V : Type v) [field K]
+lemma finrank_eq_dim (K : Type u) (V : Type v) [division_ring K]
   [add_comm_group V] [module K V] [finite_dimensional K V] :
   (finrank K V : cardinal.{v}) = module.rank K V :=
 by rw [finrank, cast_to_nat_of_lt_omega (dim_lt_omega K V)]
@@ -153,11 +162,12 @@ begin
   exact_mod_cast h,
 end
 
-lemma finrank_of_infinite_dimensional {K V : Type*} [field K] [add_comm_group V] [module K V]
+lemma finrank_of_infinite_dimensional
+  {K V : Type*} [division_ring K] [add_comm_group V] [module K V]
   (h : ¬finite_dimensional K V) : finrank K V = 0 :=
 dif_neg $ mt is_noetherian.iff_dim_lt_omega.2 h
 
-lemma finite_dimensional_of_finrank {K V : Type*} [field K] [add_comm_group V] [module K V]
+lemma finite_dimensional_of_finrank {K V : Type*} [division_ring K] [add_comm_group V] [module K V]
   (h : 0 < finrank K V) : finite_dimensional K V :=
 by { contrapose h, simp [finrank_of_infinite_dimensional h] }
 
@@ -172,13 +182,6 @@ lemma fact_finite_dimensional_of_finrank_eq_succ {K V : Type*} [field K] [add_co
   finite_dimensional K V :=
 finite_dimensional_of_finrank $ by convert nat.succ_pos n; apply fact.out
 
-/-- If a vector space has a finite basis, then its dimension (seen as a cardinal) is equal to the
-cardinality of the basis. -/
-lemma dim_eq_card_basis {ι : Type w} [fintype ι] (h : basis ι K V) :
-  module.rank K V = fintype.card ι :=
-by rw [←h.mk_range_eq_dim, cardinal.fintype_card,
-       set.card_range_of_injective h.injective]
-
 /-- If a vector space has a finite basis, then its dimension is equal to the cardinality of the
 basis. -/
 lemma finrank_eq_card_basis {ι : Type w} [fintype ι] (h : basis ι K V) :
@@ -235,28 +238,6 @@ lemma basis_unique.repr_eq_zero_iff {ι : Type*} [unique ι] {h : finrank K V =
 ⟨λ hv, (basis_unique ι h).repr.map_eq_zero_iff.mp (finsupp.ext $ λ j, subsingleton.elim i j ▸ hv),
  λ hv, by rw [hv, linear_equiv.map_zero, finsupp.zero_apply]⟩
 
-/-- In a vector space with dimension 1, each set {v} is a basis for `v ≠ 0`. -/
-noncomputable def basis_singleton (ι : Type*) [unique ι]
-  (h : finrank K V = 1) (v : V) (hv : v ≠ 0) :
-  basis ι K V :=
-let b := basis_unique ι h in
-b.map (linear_equiv.smul_of_unit (units.mk0
-  (b.repr v (default ι))
-  (mt basis_unique.repr_eq_zero_iff.mp hv)))
-
-@[simp] lemma basis_singleton_apply (ι : Type*) [unique ι]
-  (h : finrank K V = 1) (v : V) (hv : v ≠ 0) (i : ι) :
-  basis_singleton ι h v hv i = v :=
-calc basis_singleton ι h v hv i
-    = (((basis_unique ι h).repr) v) (default ι) • (basis_unique ι h) (default ι) :
-      by simp [subsingleton.elim i (default ι), basis_singleton, linear_equiv.smul_of_unit]
-... = v : by rw [← finsupp.total_unique K (basis.repr _ v), basis.total_repr]
-
-@[simp] lemma range_basis_singleton (ι : Type*) [unique ι]
-  (h : finrank K V = 1) (v : V) (hv : v ≠ 0) :
-  set.range (basis_singleton ι h v hv) = {v} :=
-by rw [set.range_unique, basis_singleton_apply]
-
 lemma cardinal_mk_le_finrank_of_linear_independent
   [finite_dimensional K V] {ι : Type w} {b : ι → V} (h : linear_independent K b) :
   cardinal.mk ι ≤ finrank K V :=
@@ -334,6 +315,90 @@ lemma finrank_zero_of_subsingleton [h : subsingleton V] :
   finrank K V = 0 :=
 finrank_zero_iff.2 h
 
+lemma basis.subset_extend {s : set V} (hs : linear_independent K (coe : s → V)) :
+  s ⊆ hs.extend (set.subset_univ _) :=
+hs.subset_extend _
+
+/-- If a submodule has maximal dimension in a finite dimensional space, then it is equal to the
+whole space. -/
+lemma eq_top_of_finrank_eq [finite_dimensional K V] {S : submodule K V}
+  (h : finrank K S = finrank K V) : S = ⊤ :=
+begin
+  set bS := basis.of_vector_space K S with bS_eq,
+  have : linear_independent K (coe : (coe '' basis.of_vector_space_index K S : set V) → V),
+    from @linear_independent.image_subtype _ _ _ _ _ _ _ _ _
+      (submodule.subtype S) (by simpa using bS.linear_independent) (by simp),
+  set b := basis.extend this with b_eq,
+  letI : fintype (this.extend _) :=
+    classical.choice (finite_of_linear_independent (by simpa using b.linear_independent)),
+  letI : fintype (subtype.val '' basis.of_vector_space_index K S) :=
+    classical.choice (finite_of_linear_independent this),
+  letI : fintype (basis.of_vector_space_index K S) :=
+    classical.choice (finite_of_linear_independent (by simpa using bS.linear_independent)),
+  have : subtype.val '' (basis.of_vector_space_index K S) = this.extend (set.subset_univ _),
+  from set.eq_of_subset_of_card_le (this.subset_extend _)
+    (by rw [set.card_image_of_injective _ subtype.val_injective, ← finrank_eq_card_basis bS,
+         ← finrank_eq_card_basis b, h]; apply_instance),
+  rw [← b.span_eq, b_eq, basis.coe_extend, subtype.range_coe, ← this, ← subtype_eq_val, span_image],
+  have := bS.span_eq,
+  rw [bS_eq, basis.coe_of_vector_space, subtype.range_coe] at this,
+  rw [this, map_top (submodule.subtype S), range_subtype],
+end
+
+variable (K)
+/-- A division_ring is one-dimensional as a vector space over itself. -/
+@[simp] lemma finrank_self : finrank K K = 1 :=
+begin
+  have := dim_self K,
+  rw [←finrank_eq_dim] at this,
+  exact_mod_cast this
+end
+
+instance finite_dimensional_self : finite_dimensional K K :=
+by apply_instance
+
+/-- The vector space of functions on a fintype ι has finrank equal to the cardinality of ι. -/
+@[simp] lemma finrank_fintype_fun_eq_card {ι : Type v} [fintype ι] :
+  finrank K (ι → K) = fintype.card ι :=
+begin
+  have : module.rank K (ι → K) = fintype.card ι := dim_fun',
+  rwa [← finrank_eq_dim, nat_cast_inj] at this,
+end
+
+/-- The vector space of functions on `fin n` has finrank equal to `n`. -/
+@[simp] lemma finrank_fin_fun {n : ℕ} : finrank K (fin n → K) = n :=
+by simp
+
+/-- The submodule generated by a finite set is finite-dimensional. -/
+theorem span_of_finite {A : set V} (hA : set.finite A) :
+  finite_dimensional K (submodule.span K A) :=
+is_noetherian_span_of_finite K hA
+
+/-- The submodule generated by a single element is finite-dimensional. -/
+instance (x : V) : finite_dimensional K (K ∙ x) := by {apply span_of_finite, simp}
+
+/-- Pushforwards of finite-dimensional submodules are finite-dimensional. -/
+instance (f : V →ₗ[K] V₂) (p : submodule K V) [h : finite_dimensional K p] :
+  finite_dimensional K (p.map f) :=
+begin
+  unfreezingI { rw [finite_dimensional, is_noetherian.iff_dim_lt_omega ] at h ⊢ },
+  rw [← cardinal.lift_lt.{v' v}],
+  rw [← cardinal.lift_lt.{v v'}] at h,
+  rw [cardinal.lift_omega] at h ⊢,
+  exact (lift_dim_map_le f p).trans_lt h
+end
+
+/-- Pushforwards of finite-dimensional submodules have a smaller finrank. -/
+lemma finrank_map_le (f : V →ₗ[K] V₂) (p : submodule K V) [finite_dimensional K p] :
+  finrank K (p.map f) ≤ finrank K p :=
+begin
+  rw [← cardinal.nat_cast_le.{max v v'}, ← cardinal.lift_nat_cast.{v' v},
+    ← cardinal.lift_nat_cast.{v v'}, finrank_eq_dim K p, finrank_eq_dim K (p.map f)],
+  exact lift_dim_map_le f p
+end
+
+variable {K}
+
 section
 open_locale big_operators
 open finset
@@ -459,90 +524,42 @@ end
 
 end
 
-lemma basis.subset_extend {s : set V} (hs : linear_independent K (coe : s → V)) :
-  s ⊆ hs.extend (set.subset_univ _) :=
-hs.subset_extend _
+end division_ring
 
-/-- If a submodule has maximal dimension in a finite dimensional space, then it is equal to the
-whole space. -/
-lemma eq_top_of_finrank_eq [finite_dimensional K V] {S : submodule K V}
-  (h : finrank K S = finrank K V) : S = ⊤ :=
-begin
-  set bS := basis.of_vector_space K S with bS_eq,
-  have : linear_independent K (coe : (coe '' basis.of_vector_space_index K S : set V) → V),
-    from @linear_independent.image_subtype _ _ _ _ _ _ _ _ _
-      (submodule.subtype S) (by simpa using bS.linear_independent) (by simp),
-  set b := basis.extend this with b_eq,
-  letI : fintype (this.extend _) :=
-    classical.choice (finite_of_linear_independent (by simpa using b.linear_independent)),
-  letI : fintype (subtype.val '' basis.of_vector_space_index K S) :=
-    classical.choice (finite_of_linear_independent this),
-  letI : fintype (basis.of_vector_space_index K S) :=
-    classical.choice (finite_of_linear_independent (by simpa using bS.linear_independent)),
-  have : subtype.val '' (basis.of_vector_space_index K S) = this.extend (set.subset_univ _),
-  from set.eq_of_subset_of_card_le (this.subset_extend _)
-    (by rw [set.card_image_of_injective _ subtype.val_injective, ← finrank_eq_card_basis bS,
-         ← finrank_eq_card_basis b, h]; apply_instance),
-  rw [← b.span_eq, b_eq, basis.coe_extend, subtype.range_coe, ← this, ← subtype_eq_val, span_image],
-  have := bS.span_eq,
-  rw [bS_eq, basis.coe_of_vector_space, subtype.range_coe] at this,
-  rw [this, map_top (submodule.subtype S), range_subtype],
-end
+section field
 
-variable (K)
-/-- A field is one-dimensional as a vector space over itself. -/
-@[simp] lemma finrank_of_field : finrank K K = 1 :=
-begin
-  have := dim_of_ring K,
-  rw [←finrank_eq_dim] at this,
-  exact_mod_cast this
-end
-
-instance finite_dimensional_self : finite_dimensional K K :=
-by apply_instance
-
-/-- The vector space of functions on a fintype ι has finrank equal to the cardinality of ι. -/
-@[simp] lemma finrank_fintype_fun_eq_card {ι : Type v} [fintype ι] :
-  finrank K (ι → K) = fintype.card ι :=
-begin
-  have : module.rank K (ι → K) = fintype.card ι := dim_fun',
-  rwa [← finrank_eq_dim, nat_cast_inj] at this,
-end
-
-/-- The vector space of functions on `fin n` has finrank equal to `n`. -/
-@[simp] lemma finrank_fin_fun {n : ℕ} : finrank K (fin n → K) = n :=
-by simp
+variables {K : Type u} {V : Type v} [field K] [add_comm_group V] [module K V]
+{V₂ : Type v'} [add_comm_group V₂] [module K V₂]
 
-/-- The submodule generated by a finite set is finite-dimensional. -/
-theorem span_of_finite {A : set V} (hA : set.finite A) :
-  finite_dimensional K (submodule.span K A) :=
-is_noetherian_span_of_finite K hA
+/-- In a vector space with dimension 1, each set {v} is a basis for `v ≠ 0`. -/
+noncomputable def basis_singleton (ι : Type*) [unique ι]
+  (h : finrank K V = 1) (v : V) (hv : v ≠ 0) :
+  basis ι K V :=
+let b := basis_unique ι h in
+b.map (linear_equiv.smul_of_unit (units.mk0
+  (b.repr v (default ι))
+  (mt basis_unique.repr_eq_zero_iff.mp hv)))
 
-/-- The submodule generated by a single element is finite-dimensional. -/
-instance (x : V) : finite_dimensional K (K ∙ x) := by {apply span_of_finite, simp}
+@[simp] lemma basis_singleton_apply (ι : Type*) [unique ι]
+  (h : finrank K V = 1) (v : V) (hv : v ≠ 0) (i : ι) :
+  basis_singleton ι h v hv i = v :=
+calc basis_singleton ι h v hv i
+    = (((basis_unique ι h).repr) v) (default ι) • (basis_unique ι h) (default ι) :
+      by simp [subsingleton.elim i (default ι), basis_singleton, linear_equiv.smul_of_unit]
+... = v : by rw [← finsupp.total_unique K (basis.repr _ v), basis.total_repr]
 
-/-- Pushforwards of finite-dimensional submodules are finite-dimensional. -/
-instance (f : V →ₗ[K] V₂) (p : submodule K V) [h : finite_dimensional K p] :
-  finite_dimensional K (p.map f) :=
-begin
-  unfreezingI { rw [finite_dimensional, is_noetherian.iff_dim_lt_omega ] at h ⊢ },
-  rw [← cardinal.lift_lt.{v' v}],
-  rw [← cardinal.lift_lt.{v v'}] at h,
-  rw [cardinal.lift_omega] at h ⊢,
-  exact (lift_dim_map_le f p).trans_lt h
-end
+@[simp] lemma range_basis_singleton (ι : Type*) [unique ι]
+  (h : finrank K V = 1) (v : V) (hv : v ≠ 0) :
+  set.range (basis_singleton ι h v hv) = {v} :=
+by rw [set.range_unique, basis_singleton_apply]
 
-/-- Pushforwards of finite-dimensional submodules have a smaller finrank. -/
-lemma finrank_map_le (f : V →ₗ[K] V₂) (p : submodule K V) [finite_dimensional K p] :
-  finrank K (p.map f) ≤ finrank K p :=
-begin
-  rw [← cardinal.nat_cast_le.{max v v'}, ← cardinal.lift_nat_cast.{v' v},
-    ← cardinal.lift_nat_cast.{v v'}, finrank_eq_dim K p, finrank_eq_dim K (p.map f)],
-  exact lift_dim_map_le f p
-end
+end field
 
 end finite_dimensional
 
+variables {K : Type u} {V : Type v} [field K] [add_comm_group V] [module K V]
+{V₂ : Type v'} [add_comm_group V₂] [module K V₂]
+
 section zero_dim
 
 open finite_dimensional
diff --git a/src/measure_theory/measure/hausdorff.lean b/src/measure_theory/measure/hausdorff.lean
index e1b819a82dc9f..1580ae1f63c8a 100644
--- a/src/measure_theory/measure/hausdorff.lean
+++ b/src/measure_theory/measure/hausdorff.lean
@@ -1227,7 +1227,7 @@ theorem dimH_univ_eq_finrank : dimH (univ : set E) = finrank ℝ E :=
 dimH_of_mem_nhds (@univ_mem _ (𝓝 0))
 
 theorem dimH_univ : dimH (univ : set ℝ) = 1 :=
-by rw [dimH_univ_eq_finrank ℝ, finite_dimensional.finrank_of_field, nat.cast_one]
+by rw [dimH_univ_eq_finrank ℝ, finite_dimensional.finrank_self, nat.cast_one]
 
 end real