(* Authors: Albert Qiaochu Jiang *) theory mathd_numbertheory_252 imports Complex_Main begin theorem mathd_numbertheory_252: "(fact 7) mod 23 = (3::nat)" sorry end