Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-11-25 00:45 6af35ecb

View on Github →

feat(topology/algebra/infinite_sum): add has_sum versions of a few tsum lemmas (#1737) Also add a few lemmas in analysis/specific_limits

Estimated changes

added theorem tsum_geometric_two'
added theorem has_sum_fintype
added theorem has_sum_single
added theorem sum_le_has_sum
added theorem sum_le_tsum