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