On Sun, 29 Dec 2019 06:59:23 -0800 (PST), Glauco <[email protected]> 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 ... > 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.
As a general rule, if someone else finds something useful in a mathbox, then we promote it to the main body (unless there's some serious known problem). Stuff in the main body is much easier to reuse and tends to be organized more logically. I'd like to see more assertions moved into the main body in general. I just updated a graph that shows the number of proven statements over time in set.mm. It shows that the mathboxes have grown much faster than the main body, which I interpret as "some things in mathboxes should be moved into the main body". The graph is here: https://docs.google.com/spreadsheets/d/1TnuBekyUP918smZeJRD0WrPhJthi915Ose0cnUnB1uc The graph certainly makes it clear that set.mm continues to grow, but I think we already knew that :-). --- David A. Wheeler -- 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/E1ilcAM-0000NO-KQ%40rmmprod07.runbox.
