Commit 2023-03-05 07:28 e84fd56d

View on Github →

feat: Port Topology.Algebra.InfiniteSum.Ring (#2640)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/Algebra/InfiniteSum/Ring.lean

added theorem Commute.tsum_left

added theorem Commute.tsum_right

added theorem HasSum.div_const

added theorem HasSum.mul

added theorem HasSum.mul_eq

added theorem HasSum.mul_left

added theorem HasSum.mul_right

added theorem Summable.div_const

added theorem Summable.mul_left

added theorem Summable.mul_right

added theorem Summable.tsum_mul_left

added theorem Summable.tsum_mul_right

added theorem hasSum_div_const_iff

added theorem hasSum_mul_left_iff

added theorem hasSum_mul_right_iff

added theorem summable_div_const_iff

added theorem summable_mul_left_iff

added theorem summable_mul_prod_iff_summable_mul_sigma_antidiagonal

added theorem summable_mul_right_iff

added theorem summable_sum_mul_antidiagonal_of_summable_mul

added theorem summable_sum_mul_range_of_summable_mul

added theorem tsum_div_const

added theorem tsum_mul_left

added theorem tsum_mul_right

added theorem tsum_mul_tsum

added theorem tsum_mul_tsum_eq_tsum_sum_antidiagonal

added theorem tsum_mul_tsum_eq_tsum_sum_range