search

leanprover-community / mathlib3

Lean 3's obsolete mathematical components library: please use mathlib4
https://leanprover-community.github.io/lean3
Apache License 2.0
1.67k stars 299 forks source link

feat(topology/algebra/infinite_sum) : define infinite products #19219

Open AntoineChambert-Loir opened 1 year ago

AntoineChambert-Loir commented 1 year ago

This is a refactor of infinite sums, more or less everything is now available in a comm_monoid via multipliable, has_tprod, tprod, and in the case of add_comm_monoid as smmable, has_sum, tsum.

Open in Gitpod

eric-wieser commented 1 year ago

As discussed on Zulip, we have a competing PR for this at #18405.