*To*: SrinivasaRao Subramanya <SrinivasaRao.Subramanya at rsise.anu.edu.au>*Subject*: Re: [isabelle] "[|prime p |] ==>(n::nat)^p = n mod p"*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Tue, 13 Feb 2007 09:55:45 +0000*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <45D0284A.2060406@rsise.anu.edu.au>*References*: <45D0284A.2060406@rsise.anu.edu.au>

Larry Paulson On 12 Feb 2007, at 08:41, SrinivasaRao Subramanya wrote:

What is an elegant and compact way to prove (Fermat's littletheorem for natural numbers)lemma "[|prime p |] ==>(n::nat)^p = n mod p" in Isabelle. Would appreciate a code snippet

**References**:**[isabelle] "[|prime p |] ==>(n::nat)^p = n mod p"***From:*SrinivasaRao Subramanya

- Previous by Date: [isabelle] MathUI 2007: Workshop on Mathematical User Interfaces, Linz, Austria, June 2007
- Next by Date: [isabelle] [Fwd: Re: [Fwd: Re: Frst order automation with external provers]]
- Previous by Thread: [isabelle] "[|prime p |] ==>(n::nat)^p = n mod p"
- Next by Thread: [isabelle] Bytecode'07: call for participation
- Cl-isabelle-users February 2007 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