chore(linear_algebra/linear_independent): use is_empty ι instead of…

… `¬nonempty ι` (#8331)

src/field_theory/fixed.lean

@@ -73,7 +73,8 @@ lemma linear_independent_smul_of_linear_independent {s : finset F} :
   linear_independent (fixed_points G F) (λ i : (↑s : set F), (i : F)) →
   linear_independent F (λ i : (↑s : set F), mul_action.to_fun G F i) :=
 begin
-  refine finset.induction_on s (λ _, linear_independent_empty_type $ λ ⟨x⟩, x.2)
+  haveI : is_empty ((∅ : finset F) : set F) := ⟨subtype.prop⟩,
+  refine finset.induction_on s (λ _, linear_independent_empty_type)
     (λ a s has ih hs, _),
   rw coe_insert at hs ⊢,
   rw linear_independent_insert (mt mem_coe.1 has) at hs,

src/linear_algebra/linear_independent.lean

@@ -150,13 +150,8 @@ theorem fintype.linear_independent_iff' [fintype ι] :
     (linear_map.lsum R (λ i : ι, R) ℕ (λ i, linear_map.id.smul_right (v i))).ker = ⊥ :=
 by simp [fintype.linear_independent_iff, linear_map.ker_eq_bot', funext_iff]
 
-lemma linear_independent_empty_type (h : ¬ nonempty ι) : linear_independent R v :=
-begin
- rw [linear_independent_iff],
- intros,
- ext i,
- exact false.elim (h ⟨i⟩)
-end
+lemma linear_independent_empty_type [is_empty ι] : linear_independent R v :=
+linear_independent_iff.mpr $ λ v hv, subsingleton.elim v 0
 
 lemma linear_independent.ne_zero [nontrivial R]
   (i : ι) (hv : linear_independent R v) : v i ≠ 0 :=
@@ -544,8 +539,7 @@ begin
   assume t, rw [set.Union, ← finset.sup_eq_supr],
   refine t.induction_on _ _,
   { rw finset.sup_empty,
-    apply linear_independent_empty_type (not_nonempty_iff_imp_false.2 _),
-    exact λ x, set.not_mem_empty x (subtype.mem x) },
+    apply linear_independent_empty_type, },
   { rintros i s his ih,
     rw [finset.sup_insert],
     refine (hl _).union ih _,

src/ring_theory/polynomial/bernstein.lean

@@ -248,8 +248,7 @@ lemma linear_independent_aux (n k : ℕ) (h : k ≤ n + 1):
   linear_independent ℚ (λ ν : fin k, bernstein_polynomial ℚ n ν) :=
 begin
   induction k with k ih,
-  { apply linear_independent_empty_type,
-    rintro ⟨⟨n, ⟨⟩⟩⟩, },
+  { apply linear_independent_empty_type, },
   { apply linear_independent_fin_succ'.mpr,
     fsplit,
     { exact ih (le_of_lt h), },