I agree. You can move these into the main part of set.mm. On Sunday, December 29, 2019 at 9:59:24 AM UTC-5, Glauco wrote: > > 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/79eea029-e1c5-4746-be9c-9eebbbcd8e87%40googlegroups.com.
