Congratulations also from my side for proving another "Metamath 100" theorem!
I also had a look at the "general theorems". I agree that a lot of them could be moved to the main part. As David (and also others) mentioned, this should be done in a structured way. At the moment, these theorems are all mixed up in section "Miscellanea", so maybe the first step would be to structure this section (using appropriate subsections, corresponding to the (sub)sections of the main part). As far as my latest "Metamath 100" theorem is concerned, I plan to move it (and all theorems which are used by its proof) to the main part, too. See issue #1314 at GitHub. Alexander On Monday, December 16, 2019 at 1:32:53 AM UTC+1, David A. Wheeler wrote: > > On Sun, 15 Dec 2019 13:02:33 -0800 (PST), Benoit <[email protected] > <javascript:>> wrote: > > Like FL, I think several lemmas deserve to be in the main part. > > I believe that all "Metamath 100" results (and thus all they depend on) > should eventually move into the main body. After all, all Metamath 100 > results are > results that at least some others believe are important. > > We don't have to do that *instantly* of course. > In many cases I expect there will be discussion as the dependencies > are examined, possibly generalized, and then moved into the main body > in groups over time. > > I think it's important to keep working on getting more things moved from > mathboxes > into the main body. Tools like mmj2 only consider items in the main body > for > many automated steps, and in any case I think it's far more sensible to > readers if major results are properly organized in the main body. > > --- 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/d4dc0251-1651-4994-88f7-96fb1d48c602%40googlegroups.com.
