[isabelle] "[|prime p |] ==>(n::nat)^p = n mod p"
What is an elegant and compact way to prove (Fermat's little theorem for
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