src/HOL/Number_Theory/Pocklington.thy
changeset 55370 e6be866b5f5b
parent 55346 d344d663658a
child 57512 cc97b347b301
equal deleted inserted replaced
55369:713629c2b73c 55370:e6be866b5f5b
   666 qed
   666 qed
   667 
   667 
   668 
   668 
   669 subsection{*Prime factorizations*}
   669 subsection{*Prime factorizations*}
   670 
   670 
   671 text{*FIXME Some overlap with material in UniqueFactorization, class unique_factorization.*}
   671 (* FIXME some overlap with material in UniqueFactorization, class unique_factorization *)
   672 
   672 
   673 definition "primefact ps n = (foldr op * ps  1 = n \<and> (\<forall>p\<in> set ps. prime p))"
   673 definition "primefact ps n = (foldr op * ps  1 = n \<and> (\<forall>p\<in> set ps. prime p))"
   674 
   674 
   675 lemma primefact: assumes n: "n \<noteq> 0"
   675 lemma primefact: assumes n: "n \<noteq> 0"
   676   shows "\<exists>ps. primefact ps n"
   676   shows "\<exists>ps. primefact ps n"