Commit 2021-03-11 17:09 998a3827

View on Github →

feat(topology/algebra/infinite_sum): add tsum_even_add_odd (#6620) Prove ∑' i, f (2 * i) + ∑' i, f (2 * i + 1) = ∑' i, f i and some supporting lemmas.

Estimated changes

Modified src/algebra/ring/basic.lean

added theorem range_two_mul

added theorem range_two_mul_add_one

Modified src/data/nat/parity.lean

added theorem nat.is_compl_even_odd

Modified src/topology/algebra/infinite_sum.lean

added theorem function.injective.has_sum_range_iff

added theorem has_sum.add_disjoint

added theorem has_sum.add_is_compl

added theorem has_sum.even_add_odd

added theorem summable.even_add_odd

added theorem tsum_even_add_odd

added theorem tsum_union_disjoint