Stream: Archive Mirror: Isabelle Users Mailing List

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

view this post on Zulip Email Gateway (Aug 18 2022 at 10:10):

From: SrinivasaRao Subramanya <SrinivasaRao.Subramanya@rsise.anu.edu.au>
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

Regards
Srinivas

view this post on Zulip Email Gateway (Aug 18 2022 at 10:10):

From: Lawrence Paulson <lp15@cam.ac.uk>
This theorem is proved (for the integers) in src/HOL/NumberTheory/
EulerFermat.thy.

Larry Paulson

Last updated: May 03 2024 at 08:18 UTC