feat: generalize Module.Finite.finite_basis to semirings (#16655)

leanprover-community · Sep 10, 2024 · a5f50bc · a5f50bc
1 parent 71f079f
commit a5f50bc
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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›