src/HOL/Number_Theory/Primes.thy
changeset 58898 1ebf0a1f12a4
parent 58889 5b7a9633cfa8
child 58954 18750e86d5b8
equal deleted inserted replaced
58897:527bd5a7e9f8 58898:1ebf0a1f12a4
   152 lemma two_is_prime_nat [simp]: "prime (2::nat)"
   152 lemma two_is_prime_nat [simp]: "prime (2::nat)"
   153   by simp
   153   by simp
   154 
   154 
   155 text{* A bit of regression testing: *}
   155 text{* A bit of regression testing: *}
   156 
   156 
   157 lemma "prime(97::nat)" by simp
   157 lemma "prime(7::nat)" by simp
   158 lemma "prime(997::nat)" by eval
   158 lemma "prime(997::nat)" by eval
   159 
   159 
   160 
   160 
   161 lemma prime_imp_power_coprime_nat: "prime p \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
   161 lemma prime_imp_power_coprime_nat: "prime p \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
   162   by (metis coprime_exp_nat gcd_nat.commute prime_imp_coprime_nat)
   162   by (metis coprime_exp_nat gcd_nat.commute prime_imp_coprime_nat)