Re: [isabelle] "[|prime p |] ==>(n::nat)^p = n mod p"

This theorem is proved (for the integers) in src/HOL/NumberTheory/ EulerFermat.thy.

Larry Paulson

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

What is an elegant and compact way to prove (Fermat's little theorem for natural numbers)

lemma "[|prime p |] ==>(n::nat)^p = n mod p"

in Isabelle.  Would appreciate a code snippet

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