# Commit 2024-03-30 22:01 f4bf34de

View on Github →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.