Skip to content

Commit d7cd016

Browse files
committed
Correct description of `finsum_mem_of_eqOn_zero` to say "sum" instead of "product"
1 parent 658f45e commit d7cd016

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

Mathlib/Algebra/BigOperators/Finprod.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -564,7 +564,7 @@ theorem finprod_mem_one (s : Set α) : (∏ᶠ i ∈ s, (1 : M)) = 1 := by simp
564564

565565
/-- If a function `f` equals `1` on a set `s`, then the product of `f i` over `i ∈ s` equals `1`. -/
566566
@[to_additive
567-
"If a function `f` equals `0` on a set `s`, then the product of `f i` over `i ∈ s`
567+
"If a function `f` equals `0` on a set `s`, then the sum of `f i` over `i ∈ s`
568568
equals `0`."]
569569
theorem finprod_mem_of_eqOn_one (hf : s.EqOn f 1) : ∏ᶠ i ∈ s, f i = 1 := by
570570
rw [← finprod_mem_one s]

0 commit comments

Comments
 (0)