Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-12-30 17:33 16320e2e

View on Github →

chore(topology/algebra/infinite_sum): refactor tsum_mul_left/right (#5533)

  • move old lemmas to summable namespace;
  • add new tsum_mul_left and tsum_mul_right that work in a division_ring without a summable assumption.

Estimated changes

added theorem has_sum.nonneg
added theorem has_sum.nonpos
added theorem summable.tsum_mul_left
modified theorem tsum_mul_left
modified theorem tsum_mul_right
added theorem nnreal.tsum_mul_left
added theorem nnreal.tsum_mul_right