fix

leanprover-community · Nov 22, 2024 · a0fa1f1 · a0fa1f1
1 parent b835204
commit a0fa1f1
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean b/Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean
@@ -123,8 +123,8 @@ lemma prod_add_prod_le {i : ι} {f g h : ι → R} (hi : i ∈ s) (h2i : g i + h
 
 end OrderedCommSemiring
 
-theorem sum_mul_self_eq_zero_iff [LinearOrderedRing R] (s : Finset ι) (f : ι → R) :
-    ∑ i ∈ s, f i * f i = 0 ↔ ∀ i ∈ s, f i = 0 := by
+theorem sum_mul_self_eq_zero_iff [LinearOrderedSemiring R] [ExistsAddOfLE R] (s : Finset ι)
+    (f : ι → R) : ∑ i ∈ s, f i * f i = 0 ↔ ∀ i ∈ s, f i = 0 := by
   rw [sum_eq_zero_iff_of_nonneg fun _ _ ↦ mul_self_nonneg _]
   simp