From a5f50bc33216ba08f7e555873f7475f1b93579e2 Mon Sep 17 00:00:00 2001
From: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Date: Tue, 10 Sep 2024 08:39:37 +0000
Subject: [PATCH] feat: generalize Module.Finite.finite_basis to semirings
 (#16655)

---
 Mathlib/RingTheory/Finiteness.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/RingTheory/Finiteness.lean b/Mathlib/RingTheory/Finiteness.lean
index 52c43e48c59b9..b9e7cb2a2c070 100644
--- a/Mathlib/RingTheory/Finiteness.lean
+++ b/Mathlib/RingTheory/Finiteness.lean
@@ -702,7 +702,7 @@ instance Module.Finite.tensorProduct [CommSemiring R] [AddCommMonoid M] [Module
   out := (TensorProduct.map₂_mk_top_top_eq_top R M N).subst (hM.out.map₂ _ hN.out)
 
 /-- If a free module is finite, then any arbitrary basis is finite. -/
-lemma Module.Finite.finite_basis {R M} [Ring R] [Nontrivial R] [AddCommGroup M] [Module R M]
+lemma Module.Finite.finite_basis {R M} [Semiring R] [Nontrivial R] [AddCommGroup M] [Module R M]
     {ι} [Module.Finite R M] (b : Basis ι R M) :
     _root_.Finite ι :=
   let ⟨s, hs⟩ := ‹Module.Finite R M›