Mathlib v3 is deprecated. Go to Mathlib v4

Theorem has_sum_single

Modification history

2019-11-25 00:45

src/topology/algebra/infinite_sum.lean

feat(topology/algebra/infinite_sum): add `has_sum` versions of a few `tsum` lemmas (#1737) …

Added has_sum_single View on Github →