Commit 2024-03-30 22:01 f4bf34de

feat: Infinite products (#11733) Last year, YaelDillies made a pull request to mathlib3 that unfortunately never got merged in: https://github.com/leanprover-community/mathlib/pull/18405. This is the mathlib4 version of that pull request. We define arbitrarily indexed products in a commutative monoid with a topology. This is done by "multiplicativizing" the currently existing definitions and theorems about arbitrarily indexed sums. That is, the existing code is rewritten in the multiplicative setting, and the original definitions and theorems are recovered using @[to_additive]. Please see this thread on Zulip for information on why this approach was chosen: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Infinite.20products As YaelDillies wrote in the description of https://github.com/leanprover-community/mathlib/pull/18405, there are a few small technical issues that arise when directly "multiplicativizing" theorems in this way:

• I have renamed cauchySeq_finset_iff_vanishing to cauchySeq_finset_iff_sum_vanishing to make the name multiplicativizable. This is slightly different from the name cauchy_seq_finset_sum_iff_vanishing that YaelDillies used, and it is meant to parallel the existing name cauchySeq_finset_iff_tsum_vanishing.
• Currently, on master, there is a theorem called tsum_sum about taking the tsum of a sum, and a theorem called tsum_prod about taking a tsum on a product of two index sets. I have called the multiplicative versions tprod_of_prod and tprod_prod. This is slightly different from the names tprod_prod'' and tprod_prod that YaelDillies used. eric-wieser suggested renaming tsum_prod to tsum_prod_index to get around this issue, which I can do in a separate pull request.