> > > job154.log:Proof of "fourierdlem45" decreased from 5709 to 53 bytes using >> "ioodvbdlimc1lem >> > ~fourierdlem45 (contributed in Dec 2019, not used!), ~ioodvbdlimc1lem > does not exist (cut off at the end?), only ~ioodvbdlimc1lem1 and > ~ioodvbdlimc1lem2 all in GS's mathbox. I think ~fourierdlem45 could be > deleted (but GS has to decide). > > ~ fourierdlem45 was originally intended as a specific lemma for ~ fourierd , but later on it was replaced by ioodvbdlimc1lem1 in order to prove ~ ioodvbdlimc1 , that will probably be useful on its own.
I suggest to apply the minimization, in order to save space ( but I plan to remove ~ fourierdlem45 in a future commit, with the proper renumbering of other lemmas ) Thanks for your analysis 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/96086006-5d0a-4691-bb36-2372064cddbf%40googlegroups.com.
