chore(LinearAlgebra/LinearIndependent): generalize a section from rin…

…gs to semirings (#17864)
leanprover-community · Oct 17, 2024 · 628c756 · 628c756
1 parent 52caeb5
commit 628c756
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Mathlib/LinearAlgebra/LinearIndependent.lean b/Mathlib/LinearAlgebra/LinearIndependent.lean
@@ -1183,7 +1183,7 @@ end Module
 
 section Nontrivial
 
-variable [Ring R] [Nontrivial R] [AddCommGroup M] [AddCommGroup M']
+variable [Semiring R] [Nontrivial R] [AddCommGroup M] [AddCommGroup M']
 variable [Module R M] [NoZeroSMulDivisors R M] [Module R M']
 variable {s t : Set M}