infinite_sum): add `tsum_even_add_odd` (#6620)

Commit

5 years ago

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.

Author

urkud

Parents

95a8e958

mathlib 998a3827 - feat(topology/algebra/infinite_sum): add `tsum_even_add_odd` (#6620)

mathlib
998a3827 - feat(topology/algebra/infinite_sum): add `tsum_even_add_odd` (#6620)