mathlib3
54af9e9b - fix(topology/algebra/infinite_sum): `tsum_neg` doesn't need `summable` (#13950)

Commit
3 years ago
fix(topology/algebra/infinite_sum): `tsum_neg` doesn't need `summable` (#13950) Both sides are 0 in the not-summable case.
Author
Parents
Loading