Re: [isabelle] square root

I am currently in the process of revising the Number Theory library from the bottom up, and expect to have a significantly cleaner and expanded library over the summer.

But the short answer to your question is that the theorem you mention isn't there yet. It should be easy to prove: if x is a square root of a mod p, then p - x is another one, and it is not hard to show that these can't be congruent mod p.

Jeremy Avigad

kuecuek at wrote:

is there any proof or definition about the square roots?

i want to show If p is an odd prime and a is a Quadratishe residue mod p (EX x. [x^² = a] (mod p)) then a has exactly two square roots modulo p.

i have found some definition about the Quadres in Numbertheory/residues but there isn't any lemma about square roots there.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.