Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-09 14:41 766146b9

View on Github →

fix(topology/algebra/infinite_sum): remove hard-coding of ℕ and ℝ (#6096) It may be possible to make these assumptions stricter, but they're weak enough to still cover the original use case. Hopefully that can be handled by @alexjbest's upcoming linter to relax assumptions.

Estimated changes

added theorem has_sum.update
added theorem has_sum_lt
added theorem has_sum_mono
added theorem has_sum_strict_mono
added theorem summable.update
modified theorem tsum_lt_tsum
added theorem tsum_mono
added theorem tsum_strict_mono