Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-02-03 11:16 bed4f052

View on Github →

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

Estimated changes

added theorem has_sum_pi_single
added theorem tsum_pi_single