The build has completed at http://us2.metamath.org/mpeuni/mmrecent.html. Glauco's update adds about 1.5MB (20K lines) to set.mm, comprising over 400 new theorems (and no new definitions). Hopefully he'll give us an outline of what it all does.
Norm On Saturday, December 14, 2019 at 10:01:03 AM UTC-5, David A. Wheeler wrote: > > I am very pleased to announce that the Fourier series convergence, > Metamath 100#76, has been proven by Glauco. This is a tremendous > achievement and I congratulate him. > > There are a few cleanups and such to be done before it gets merged in, but > I expect it to be merged soon. If you're curious to see it, it is here: > > https://github.com/metamath/set.mm/pull/1317 > > I may be delayed before I add it to the official metamath 100 list and > such, but I will certainly do it. > > Congrats! > --- 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/8d513439-b571-46fc-b50c-e2a1fd3b3c53%40googlegroups.com.
