chore(linear_algebra/*): Lint (#16362)

Satisfy the `fintype_finite` and `fails_quickly` linters.

Author: YaelDillies

src/geometry/euclidean/basic.lean

@@ -783,6 +783,8 @@ lemma orthogonal_projection_fn_vsub_mem_direction_orthogonal {s : affine_subspac
 direction_mk' p s.directionᗮ ▸
   vsub_mem_direction (orthogonal_projection_fn_mem_orthogonal p) (self_mem_mk' _ _)
 
+local attribute [instance] affine_subspace.to_add_torsor
+
 /-- The orthogonal projection of a point onto a nonempty affine
 subspace, whose direction is complete. The corresponding linear map
 (mapping a vector to the difference between the projections of two

src/geometry/euclidean/circumcenter.lean

@@ -377,6 +377,8 @@ begin
           (λ i, hr i (set.mem_univ _))).symm
 end
 
+local attribute [instance] affine_subspace.to_add_torsor
+
 /-- The orthogonal projection of a point `p` onto the hyperplane spanned by the simplex's points. -/
 def orthogonal_projection_span {n : ℕ} (s : simplex ℝ P n) :
   P →ᵃ[ℝ] affine_span ℝ (set.range s.points) :=

src/linear_algebra/affine_space/affine_subspace.lean

@@ -376,7 +376,9 @@ begin
     exact vsub_mem_direction hp hq2 }
 end
 
-instance to_add_torsor (s : affine_subspace k P) [nonempty s] : add_torsor s.direction s :=
+/-- This is not an instance because it loops with `add_torsor.nonempty`. -/
+@[reducible] -- See note [reducible non instances]
+def to_add_torsor (s : affine_subspace k P) [nonempty s] : add_torsor s.direction s :=
 { vadd := λ a b, ⟨(a:V) +ᵥ (b:P), vadd_mem_of_mem_direction a.2 b.2⟩,
   zero_vadd := by simp,
   add_vadd := λ a b c, by { ext, apply add_vadd },
@@ -385,6 +387,8 @@ instance to_add_torsor (s : affine_subspace k P) [nonempty s] : add_torsor s.dir
   vsub_vadd' := λ a b, by { ext, apply add_torsor.vsub_vadd' },
   vadd_vsub' := λ a b, by { ext, apply add_torsor.vadd_vsub' } }
 
+local attribute [instance] to_add_torsor
+
 @[simp, norm_cast] lemma coe_vsub (s : affine_subspace k P) [nonempty s] (a b : s) :
   ↑(a -ᵥ b) = (a:P) -ᵥ (b:P) :=
 rfl

src/linear_algebra/affine_space/finite_dimensional.lean

@@ -39,13 +39,13 @@ span_of_finite k $ h.vsub h
 
 /-- The `vector_span` of a family indexed by a `fintype` is
 finite-dimensional. -/
-instance finite_dimensional_vector_span_of_fintype [fintype ι] (p : ι → P) :
+instance finite_dimensional_vector_span_range [_root_.finite ι] (p : ι → P) :
   finite_dimensional k (vector_span k (set.range p)) :=
 finite_dimensional_vector_span_of_finite k (set.finite_range _)
 
 /-- The `vector_span` of a subset of a family indexed by a `fintype`
 is finite-dimensional. -/
-instance finite_dimensional_vector_span_image_of_fintype [fintype ι] (p : ι → P)
+instance finite_dimensional_vector_span_image_of_finite [_root_.finite ι] (p : ι → P)
   (s : set ι) : finite_dimensional k (vector_span k (p '' s)) :=
 finite_dimensional_vector_span_of_finite k (set.to_finite _)
 
@@ -57,13 +57,13 @@ lemma finite_dimensional_direction_affine_span_of_finite {s : set P} (h : set.fi
 
 /-- The direction of the affine span of a family indexed by a
 `fintype` is finite-dimensional. -/
-instance finite_dimensional_direction_affine_span_of_fintype [fintype ι] (p : ι → P) :
+instance finite_dimensional_direction_affine_span_range [_root_.finite ι] (p : ι → P) :
   finite_dimensional k (affine_span k (set.range p)).direction :=
 finite_dimensional_direction_affine_span_of_finite k (set.finite_range _)
 
 /-- The direction of the affine span of a subset of a family indexed
 by a `fintype` is finite-dimensional. -/
-instance finite_dimensional_direction_affine_span_image_of_fintype [fintype ι] (p : ι → P)
+instance finite_dimensional_direction_affine_span_image_of_finite [_root_.finite ι] (p : ι → P)
   (s : set ι) : finite_dimensional k (affine_span k (p '' s)).direction :=
 finite_dimensional_direction_affine_span_of_finite k (set.to_finite _)
 

src/linear_algebra/alternating.lean

@@ -956,7 +956,7 @@ section basis
 
 open alternating_map
 
-variables {ι₁ : Type*} [fintype ι]
+variables {ι₁ : Type*} [finite ι]
 variables {R' : Type*} {N₁ N₂ : Type*} [comm_semiring R'] [add_comm_monoid N₁] [add_comm_monoid N₂]
 variables [module R' N₁] [module R' N₂]
 

src/linear_algebra/determinant.lean

@@ -246,11 +246,10 @@ begin
     simp [coe_det, H, this] }
 end
 
-lemma det_zero' {ι : Type*} [fintype ι] [nonempty ι] (b : basis ι A M) :
+lemma det_zero' {ι : Type*} [finite ι] [nonempty ι] (b : basis ι A M) :
   linear_map.det (0 : M →ₗ[A] M) = 0 :=
-by { haveI := classical.dec_eq ι,
-     rw [← det_to_matrix b, linear_equiv.map_zero, det_zero],
-     assumption }
+by { haveI := classical.dec_eq ι, casesI nonempty_fintype ι,
+     rwa [← det_to_matrix b, linear_equiv.map_zero, det_zero] }
 
 /-- In a finite-dimensional vector space, the zero map has determinant `1` in dimension `0`,
 and `0` otherwise. We give a formula that also works in infinite dimension, where we define
@@ -491,11 +490,14 @@ begin
   simp [alternating_map.map_perm, basis.det_self]
 end
 
-@[simp] lemma alternating_map.map_basis_eq_zero_iff (f : alternating_map R M R ι) :
+@[simp] lemma alternating_map.map_basis_eq_zero_iff {ι : Type*} [decidable_eq ι] [finite ι]
+  (e : basis ι R M) (f : alternating_map R M R ι) :
   f e = 0 ↔ f = 0 :=
-⟨λ h, by simpa [h] using f.eq_smul_basis_det e, λ h, h.symm ▸ alternating_map.zero_apply _⟩
+⟨λ h, by { casesI nonempty_fintype ι, simpa [h] using f.eq_smul_basis_det e },
+  λ h, h.symm ▸ alternating_map.zero_apply _⟩
 
-lemma alternating_map.map_basis_ne_zero_iff (f : alternating_map R M R ι) :
+lemma alternating_map.map_basis_ne_zero_iff {ι : Type*} [decidable_eq ι] [finite ι]
+  (e : basis ι R M) (f : alternating_map R M R ι) :
   f e ≠ 0 ↔ f ≠ 0 :=
 not_congr $ f.map_basis_eq_zero_iff e
 

src/linear_algebra/dimension.lean

@@ -988,19 +988,21 @@ begin
 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)) :=
+lemma dim_pi [finite η] : module.rank K (Πi, φ i) = cardinal.sum (λi, module.rank K (φ i)) :=
 begin
+  casesI nonempty_fintype η,
   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 [← (b _).mk_range_eq_dim]
 end
 
+variable [fintype η]
+
 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.mk_fintype]

src/linear_algebra/dual.lean

@@ -171,19 +171,15 @@ end
 theorem to_dual_ker : b.to_dual.ker = ⊥ :=
 ker_eq_bot'.mpr b.to_dual_inj
 
-theorem to_dual_range [fin : fintype ι] : b.to_dual.range = ⊤ :=
+theorem to_dual_range [_root_.finite ι] : b.to_dual.range = ⊤ :=
 begin
-  rw eq_top_iff',
-  intro f,
+  casesI nonempty_fintype ι,
+  refine eq_top_iff'.2 (λ f, _),
   rw linear_map.mem_range,
-  let lin_comb : ι →₀ R := finsupp.on_finset fin.elems (λ i, f.to_fun (b i)) _,
-  { use finsupp.total ι M R b lin_comb,
-    apply b.ext,
-    { intros i,
-      rw [b.to_dual_eq_repr _ i, repr_total b],
-      { refl } } },
-  { intros a _,
-    apply fin.complete }
+  let lin_comb : ι →₀ R := finsupp.equiv_fun_on_fintype.2 (λ i, f.to_fun (b i)),
+  refine ⟨finsupp.total ι M R b lin_comb, b.ext $ λ i, _⟩,
+  rw [b.to_dual_eq_repr _ i, repr_total b],
+  refl,
 end
 
 end comm_semiring
@@ -207,53 +203,52 @@ section comm_ring
 variables [comm_ring R] [add_comm_group M] [module R M] [decidable_eq ι]
 variables (b : basis ι R M)
 
+section finite
+variables [_root_.finite ι]
+
 /-- A vector space is linearly equivalent to its dual space. -/
 @[simps]
-def to_dual_equiv [fintype ι] : M ≃ₗ[R] (dual R M) :=
+def to_dual_equiv : M ≃ₗ[R] dual R M :=
 linear_equiv.of_bijective b.to_dual
   (ker_eq_bot.mp b.to_dual_ker) (range_eq_top.mp b.to_dual_range)
 
 /-- Maps a basis for `V` to a basis for the dual space. -/
-def dual_basis [fintype ι] : basis ι R (dual R M) :=
-b.map b.to_dual_equiv
+def dual_basis : basis ι R (dual R M) := b.map b.to_dual_equiv
 
 -- We use `j = i` to match `basis.repr_self`
-lemma dual_basis_apply_self [fintype ι] (i j : ι) :
-  b.dual_basis i (b j) = if j = i then 1 else 0 :=
+lemma dual_basis_apply_self (i j : ι) : b.dual_basis i (b j) = if j = i then 1 else 0 :=
 by { convert b.to_dual_apply i j using 2, rw @eq_comm _ j i }
 
-lemma total_dual_basis [fintype ι] (f : ι →₀ R) (i : ι) :
+lemma total_dual_basis (f : ι →₀ R) (i : ι) :
   finsupp.total ι (dual R M) R b.dual_basis f (b i) = f i :=
 begin
+  casesI nonempty_fintype ι,
   rw [finsupp.total_apply, finsupp.sum_fintype, linear_map.sum_apply],
   { simp_rw [linear_map.smul_apply, smul_eq_mul, dual_basis_apply_self, mul_boole,
       finset.sum_ite_eq, if_pos (finset.mem_univ i)] },
   { intro, rw zero_smul },
 end
 
-lemma dual_basis_repr [fintype ι] (l : dual R M) (i : ι) :
-  b.dual_basis.repr l i = l (b i) :=
+lemma dual_basis_repr (l : dual R M) (i : ι) : b.dual_basis.repr l i = l (b i) :=
 by rw [← total_dual_basis b, basis.total_repr b.dual_basis l]
 
-lemma dual_basis_equiv_fun [fintype ι] (l : dual R M) (i : ι) :
-  b.dual_basis.equiv_fun l i = l (b i) :=
-by rw [basis.equiv_fun_apply, dual_basis_repr]
-
-lemma dual_basis_apply [fintype ι] (i : ι) (m : M) : b.dual_basis i m = b.repr m i :=
-b.to_dual_apply_right i m
+lemma dual_basis_apply (i : ι) (m : M) : b.dual_basis i m = b.repr m i := b.to_dual_apply_right i m
 
-@[simp] lemma coe_dual_basis [fintype ι] :
-  ⇑b.dual_basis = b.coord :=
-by { ext i x, apply dual_basis_apply }
+@[simp] lemma coe_dual_basis : ⇑b.dual_basis = b.coord := by { ext i x, apply dual_basis_apply }
 
-@[simp] lemma to_dual_to_dual [fintype ι] :
-  b.dual_basis.to_dual.comp b.to_dual = dual.eval R M :=
+@[simp] lemma to_dual_to_dual : b.dual_basis.to_dual.comp b.to_dual = dual.eval R M :=
 begin
   refine b.ext (λ i, b.dual_basis.ext (λ j, _)),
   rw [linear_map.comp_apply, to_dual_apply_left, coe_to_dual_self, ← coe_dual_basis,
       dual.eval_apply, basis.repr_self, finsupp.single_apply, dual_basis_apply_self]
 end
 
+end finite
+
+lemma dual_basis_equiv_fun [fintype ι] (l : dual R M) (i : ι) :
+  b.dual_basis.equiv_fun l i = l (b i) :=
+by rw [basis.equiv_fun_apply, dual_basis_repr]
+
 theorem eval_ker {ι : Type*} (b : basis ι R M) :
   (dual.eval R M).ker = ⊥ :=
 begin
@@ -263,20 +258,20 @@ begin
   exact (basis.forall_coord_eq_zero_iff _).mp (λ i, hm (b.coord i))
 end
 
-lemma eval_range {ι : Type*} [fintype ι] (b : basis ι R M) :
-  (eval R M).range = ⊤ :=
+lemma eval_range {ι : Type*} [_root_.finite ι] (b : basis ι R M) : (eval R M).range = ⊤ :=
 begin
   classical,
+  casesI nonempty_fintype ι,
   rw [← b.to_dual_to_dual, range_comp, b.to_dual_range, map_top, to_dual_range _],
   apply_instance
 end
 
 /-- A module with a basis is linearly equivalent to the dual of its dual space. -/
-def eval_equiv  {ι : Type*} [fintype ι] (b : basis ι R M) : M ≃ₗ[R] dual R (dual R M) :=
+def eval_equiv  {ι : Type*} [_root_.finite ι] (b : basis ι R M) : M ≃ₗ[R] dual R (dual R M) :=
 linear_equiv.of_bijective (eval R M)
   (ker_eq_bot.mp b.eval_ker) (range_eq_top.mp b.eval_range)
 
-@[simp] lemma eval_equiv_to_linear_map {ι : Type*} [fintype ι] (b : basis ι R M) :
+@[simp] lemma eval_equiv_to_linear_map {ι : Type*} [_root_.finite ι] (b : basis ι R M) :
   (b.eval_equiv).to_linear_map = dual.eval R M := rfl
 
 section
@@ -294,16 +289,17 @@ end
 end comm_ring
 
 /-- `simp` normal form version of `total_dual_basis` -/
-@[simp] lemma total_coord [comm_ring R] [add_comm_group M] [module R M] [fintype ι]
+@[simp] lemma total_coord [comm_ring R] [add_comm_group M] [module R M] [_root_.finite ι]
   (b : basis ι R M) (f : ι →₀ R) (i : ι) :
   finsupp.total ι (dual R M) R b.coord f (b i) = f i :=
 by { haveI := classical.dec_eq ι, rw [← coe_dual_basis, total_dual_basis] }
 
--- TODO(jmc): generalize to rings, once `module.rank` is generalized
-theorem dual_dim_eq [field K] [add_comm_group V] [module K V] [fintype ι] (b : basis ι K V) :
+lemma dual_dim_eq [comm_ring K] [add_comm_group V] [module K V] [_root_.finite ι]
+  (b : basis ι K V) :
   cardinal.lift (module.rank K V) = module.rank K (dual K V) :=
 begin
   classical,
+  casesI nonempty_fintype ι,
   have := linear_equiv.lift_dim_eq b.to_dual_equiv,
   simp only [cardinal.lift_umax] at this,
   rw [this, ← cardinal.lift_umax],

src/linear_algebra/finsupp_vector_space.lean

@@ -200,7 +200,8 @@ begin
     ... = _ : by rw [← cardinal.lift_inj.1 hs.mk_eq_dim, cardinal.power_def]
 end
 
-lemma cardinal_lt_aleph_0_of_finite_dimensional [fintype K] [finite_dimensional K V] : #V < ℵ₀ :=
+lemma cardinal_lt_aleph_0_of_finite_dimensional [_root_.finite K] [finite_dimensional K V] :
+  #V < ℵ₀ :=
 begin
   letI : is_noetherian K V := is_noetherian.iff_fg.2 infer_instance,
   rw cardinal_mk_eq_cardinal_mk_field_pow_dim K V,

src/linear_algebra/free_module/finite/basic.lean

@@ -59,22 +59,22 @@ begin
     (linear_map.to_matrix (module.free.choose_basis R M) (module.free.choose_basis R N)).symm,
 end
 
-variables {R M}
+variables {R}
 
 /-- A free module with a basis indexed by a `fintype` is finite. -/
-lemma _root_.module.finite.of_basis {R : Type*} {M : Type*} {ι : Type*} [comm_ring R]
-  [add_comm_group M] [module R M] [fintype ι] (b : basis ι R M) : module.finite R M :=
+lemma _root_.module.finite.of_basis {R M ι : Type*} [comm_ring R] [add_comm_group M] [module R M]
+  [finite ι] (b : basis ι R M) : module.finite R M :=
 begin
+  casesI nonempty_fintype ι,
   classical,
   refine ⟨⟨finset.univ.image b, _⟩⟩,
   simp only [set.image_univ, finset.coe_univ, finset.coe_image, basis.span_eq],
 end
 
-instance _root_.module.finite.matrix {ι₁ : Type*} [fintype ι₁] {ι₂ : Type*} [fintype ι₂] :
+instance _root_.module.finite.matrix {ι₁ ι₂ : Type*} [finite ι₁] [finite ι₂] :
   module.finite R (matrix ι₁ ι₂ R) :=
-module.finite.of_basis $ pi.basis $ λ i, pi.basis_fun R _
-
-variables (M)
+by { casesI nonempty_fintype ι₁, casesI nonempty_fintype ι₂,
+  exact module.finite.of_basis (pi.basis $ λ i, pi.basis_fun R _) }
 
 instance _root_.module.finite.linear_map [module.finite R M] [module.finite R N] :
   module.finite R (M →ₗ[R] N) :=