Commit 2025-11-04 14:52 5b49109b
View on Github →typo in a docstring 1 -> 0 as a dummy value for tsum (#31260)
Confirmed by:
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Topology/Algebra/InfiniteSum/Defs.html#tsum_eq_zero_of_not_summable
