isabelle/valid/mathd_numbertheory_739.thy (
10
lines of code) (
raw
):
(* Authors: Albert Qiaochu Jiang *) theory mathd_numbertheory_739 imports Complex_Main begin theorem mathd_numbertheory_739: "(fact 9) mod 10 = (0::nat)" sorry end