[isabelle] square root


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.