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.
kuecuek at rbg.informatik.tu-darmstadt.de 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