equal
deleted
inserted
replaced
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" |