From 4155665200057b2cdf229efb96ec856858a20e35 Mon Sep 17 00:00:00 2001
From: Julian-Kuelshammer <julian.kuelshammer@math.uu.se>
Date: Sat, 16 Jan 2021 17:42:12 +0000
Subject: [PATCH] refactor(linear_algebra/dual): replace dim<omega by
 finite_dimensional (#5775)

---
 src/linear_algebra/dual.lean | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/linear_algebra/dual.lean b/src/linear_algebra/dual.lean
index da7290cd67113..b6420d1b5cda6 100644
--- a/src/linear_algebra/dual.lean
+++ b/src/linear_algebra/dual.lean
@@ -250,7 +250,7 @@ namespace vector_space
 universes u v
 variables {K : Type u} {V : Type v}
 variables [field K] [add_comm_group V] [vector_space K V]
-open module module.dual submodule linear_map cardinal is_basis
+open module module.dual submodule linear_map cardinal is_basis finite_dimensional
 
 theorem eval_ker : (eval K V).ker = ⊥ :=
 begin
@@ -267,27 +267,27 @@ begin
   exact one_ne_zero hx
 end
 
-theorem dual_dim_eq (h : dim K V < omega) :
+theorem dual_dim_eq [finite_dimensional K V] :
   cardinal.lift.{v u} (dim K V) = dim K (dual K V) :=
 begin
   classical,
-  rcases exists_is_basis_fintype h with ⟨b, hb, ⟨hf⟩⟩,
+  rcases exists_is_basis_fintype (dim_lt_omega K V) with ⟨b, hb, ⟨hf⟩⟩,
   resetI,
   exact hb.dual_dim_eq
 end
 
 
-lemma erange_coe (h : dim K V < omega) : (eval K V).range = ⊤ :=
+lemma erange_coe [finite_dimensional K V] : (eval K V).range = ⊤ :=
 begin
   classical,
-  rcases exists_is_basis_fintype h with ⟨b, hb, ⟨hf⟩⟩,
+  rcases exists_is_basis_fintype (dim_lt_omega K V) with ⟨b, hb, ⟨hf⟩⟩,
   unfreezingI { rw [← hb.to_dual_to_dual, range_comp, hb.to_dual_range, map_top, to_dual_range _] },
   apply_instance
 end
 
 /-- A vector space is linearly equivalent to the dual of its dual space. -/
-def eval_equiv (h : dim K V < omega) : V ≃ₗ[K] dual K (dual K V) :=
-linear_equiv.of_bijective (eval K V) eval_ker (erange_coe h)
+def eval_equiv [finite_dimensional K V] : V ≃ₗ[K] dual K (dual K V) :=
+linear_equiv.of_bijective (eval K V) eval_ker (erange_coe)
 
 end vector_space