Glad to find something helpful :) Re searching maybe an example would be helpful. So I was looking through the web page and scrolled up to ghomid <http://us.metamath.org/mpeuni/ghomid.html> and I wanted to find if the same concept is proven elsewhere. I guess I'd appreciate a tutorial for how others would go about that.
The sort of things I do: Open set.mm in a text editor and ctrl+f for specific phrases, like group homomorphism and then check the results. Try to open what might be relevant pages on the website and scroll through them and read to see if there are any there, this can be time consuming. Search google in the hopes it will find the right page on the website. Things maybe I should try more of if they are better: Using the MMJ2 search function. Using metamath.exe search function. I think the right partner for it is ghmid <http://us.metamath.org/mpegif/ghmid.html> which I found by writing a python script which goes through set.mm and finds all theorems which contain "group", "homomorphism" and "identity" in their description. I wrote a script which can compare the descriptions of two statements for general similarity however as you can see they are sufficiently differently worded to mean that technique didn't work so well. In general any tips on searching would be really appreciated, thanks :) -- 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/b6b20f0f-c642-4bb3-ac1d-04fa4f2fe6ed%40googlegroups.com.
