> As a side note, Tirix is now close to completing the proof of the Eckmann-Hilton argument, and although his version is better organized than mine, it still looks pretty long. I guess now we can say that the short proof on Wikipedia doesn't convey a good idea about the amount of work needed to accomplish that task.
Yes, I'm surprised that this is the case, probably shows the lack of intuition on my side. When I showed the problem set to Mario, he suggested rewriting some statements with class variables, i.e. instead of* "A. a e. B A. b e. B ( a .o. b ) = ( b .o. a)" *one can introduce *"X e. B"* and *"Y e. B"* as hypotheses and write *"( X .o. Y ) = ( Y .o. X )"*. In the end I did that only for a couple of first problems, since I wasn't sure how these additional hypotheses work with scoping etc. Thierry is using that technique in his repository, yet it seems the overall proof length is also large. I plan to add another 3 "bonus" tasks near the end of next week, asking to prove the Mendelsohn-Padmanabhan identity in a boolean group (so we get a full characterization). Again, this is trivial mathematically but I'm not quite sure it will be trivial in metamath, although we have all the required definitions like group exponent (gEx) ready. -- 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 visit https://groups.google.com/d/msgid/metamath/456ab71d-ba39-4534-8357-2ee29ec62a8cn%40googlegroups.com.
