I was checking if, recently, something similar to sum_ was added for multiplication, and I found these sections in Scott Fenton's mathbox:
21.8.8 Complex products 21.8.9 Finite products 21.8.10 Infinite products Scott Fentons's comment for df-prod is "Define the product of a series with an index set of integers A. This definition takes most of the aspects of df-sum 13322 and adapts them for multiplication instead of addition. However, we insist that in the infinite case, there is a non-zero tail of the sequence. This ensures that the convergence criteria match those of infinite sums." (but prod_ also handles effectively products "indexed" by generic finite sets) I've written a few theorems based on Scott Fenton's definition and theorems (only for finite products, for now) and it looks like we can really build a complete library, similar to what's available for sum_ (Scott already did most of the work) I keep finding proofs that require finite products (and, occasionally, even infinite products), so I hope those sections could be promoted to the main part. Of course, if Scott Fenton doesn't object (I don't know if he expected to tweak some parts of those sections, I've only "tested" some theorems of the finite product part and the section looks really well written and useful) Glauco -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/abe8f5ad-8e6d-4a3d-a4f8-da5a640f3b6e%40googlegroups.com.
