chore(StdBasis): Fintype -> Finite (#10914)

Mathlib/LinearAlgebra/StdBasis.lean

@@ -299,13 +299,14 @@ end Pi
 
 namespace Module
 
-variable (ι R M N : Type*) [Fintype ι] [CommSemiring R]
+variable (ι R M N : Type*) [Finite ι] [CommSemiring R]
   [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N]
 
 /-- The natural linear equivalence: `Mⁱ ≃ Hom(Rⁱ, M)` for an `R`-module `M`. -/
 noncomputable def piEquiv : (ι → M) ≃ₗ[R] ((ι → R) →ₗ[R] M) := Basis.constr (Pi.basisFun R ι) R
 
-lemma piEquiv_apply_apply (v : ι → M) (w : ι → R) :
+lemma piEquiv_apply_apply (ι R M : Type*) [Fintype ι] [CommSemiring R]
+    [AddCommMonoid M] [Module R M] (v : ι → M) (w : ι → R) :
     piEquiv ι R M v w = ∑ i, w i • v i := by
   simp only [piEquiv, Basis.constr_apply_fintype, Basis.equivFun_apply]
   congr