infinite_sum): lemmas about pi.single (#18360)

Commit

3 years ago

chore(topology/algebra/infinite_sum): lemmas about pi.single (#18360) The naming is consistent with `finset.sum_pi_single`.

Author

eric-wieser

Parents