*To*: kuecuek at rbg.informatik.tu-darmstadt.de*Subject*: Re: [isabelle] square root*From*: Jeremy Avigad <avigad at cmu.edu>*Date*: Wed, 08 Feb 2006 11:35:05 -0500*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <200602071110.04285.kuecuek@rbg.informatik.tu-darmstadt.de>*References*: <200602071110.04285.kuecuek@rbg.informatik.tu-darmstadt.de>*User-agent*: Mozilla Thunderbird 1.0.7 (Windows/20050923)

Jeremy Avigad kuecuek at rbg.informatik.tu-darmstadt.de wrote:

hallo is there any proof or definition about the square roots?i want to showIf 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 butthere isn't any lemma about square roots there.thanks

**References**:**[isabelle] square root***From:*kuecuek

- Previous by Date: [isabelle] nested \<^bsub> .. \<^esub>
- Next by Date: Re: [isabelle] datatype definition performance
- Previous by Thread: [isabelle] square root
- Next by Thread: [isabelle] datatype definition performance
- Cl-isabelle-users February 2006 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list