Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2017-09-13 14:20 0b163365

View on Github →

feat(topology/infinite_sum): strengten bijection proof

Estimated changes

Modified topology/infinite_sum.lean

added theorem tsum_eq_tsum_of_ne_zero

modified theorem tsum_zero