Skip to content

Commit 5b49109

Browse files

File tree

1 file changed

+1
-1
lines changed
  • Mathlib/Topology/Algebra/InfiniteSum

1 file changed

+1
-1
lines changed

Mathlib/Topology/Algebra/InfiniteSum/Defs.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -128,7 +128,7 @@ satisfying `HasProd f a`. Similar remarks apply to more general summation filter
128128
@[to_additive /-- `∑' i, f i` is the unconditional sum of `f` if it exists, or 0 otherwise.
129129
130130
More generally, if `L` is a `SummationFilter`, `∑'[L] i, f i` is the sum of `f` with respect to
131-
`L` if it exists, and `1` otherwise.
131+
`L` if it exists, and `0` otherwise.
132132
133133
(Note that even if the unconditional sum exists, it might not be unique if the topology is not
134134
separated. When the support of `f` is finite, we make the most reasonable choice, to use the sum

0 commit comments

Comments
 (0)