Hi Alexander, Theorem ~ lgsquadlem2 seems to be similar to Gauss' Lemma. Wikipedia also mentions it <https://en.wikipedia.org/wiki/Proofs_of_quadratic_reciprocity#Eisenstein's_proof> in its entry on Eisenstein proof of the quadratic reciprocity: /This result is very similar to Gauss's lemma, and can be proved in a similar fashion./
After a bit more consideration though, it does not seem to me that it is easy to derive Gauss' lemma from it. This would leave you with proving Gauss' lemma. Or, if you don't mind cooperation, you could call for someone in the community to prove Gauss' lemma while you continue on Fermat numbers. BR, _ Thierry -- 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/8d5c8932-a647-f758-858e-7fc77d40f6c0%40gmx.net.
