776 unfolding factor_def by auto |
776 unfolding factor_def by auto |
777 hence "\<one> = b \<otimes> b'" |
777 hence "\<one> = b \<otimes> b'" |
778 by (metis A(1) l_cancel m_closed m_lcomm one_closed r_one c) |
778 by (metis A(1) l_cancel m_closed m_lcomm one_closed r_one c) |
779 thus "b \<in> Units G" |
779 thus "b \<in> Units G" |
780 using A(1) Units_one_closed b'(1) unit_factor by presburger |
780 using A(1) Units_one_closed b'(1) unit_factor by presburger |
|
781 qed |
|
782 |
|
783 lemma (in comm_monoid_cancel) prime_pow_divides_iff: |
|
784 assumes "p \<in> carrier G" "a \<in> carrier G" "b \<in> carrier G" and "prime G p" and "\<not> (p divides a)" |
|
785 shows "(p [^] (n :: nat)) divides (a \<otimes> b) \<longleftrightarrow> (p [^] n) divides b" |
|
786 proof |
|
787 assume "(p [^] n) divides b" thus "(p [^] n) divides (a \<otimes> b)" |
|
788 using divides_prod_l[of "p [^] n" b a] assms by simp |
|
789 next |
|
790 assume "(p [^] n) divides (a \<otimes> b)" thus "(p [^] n) divides b" |
|
791 proof (induction n) |
|
792 case 0 with \<open>b \<in> carrier G\<close> show ?case |
|
793 by (simp add: unit_divides) |
|
794 next |
|
795 case (Suc n) |
|
796 hence "(p [^] n) divides (a \<otimes> b)" and "(p [^] n) divides b" |
|
797 using assms(1) divides_prod_r by auto |
|
798 with \<open>(p [^] (Suc n)) divides (a \<otimes> b)\<close> obtain c d |
|
799 where c: "c \<in> carrier G" and "b = (p [^] n) \<otimes> c" |
|
800 and d: "d \<in> carrier G" and "a \<otimes> b = (p [^] (Suc n)) \<otimes> d" |
|
801 using assms by blast |
|
802 hence "(p [^] n) \<otimes> (a \<otimes> c) = (p [^] n) \<otimes> (p \<otimes> d)" |
|
803 using assms by (simp add: m_assoc m_lcomm) |
|
804 hence "a \<otimes> c = p \<otimes> d" |
|
805 using c d assms(1) assms(2) l_cancel by blast |
|
806 with \<open>\<not> (p divides a)\<close> and \<open>prime G p\<close> have "p divides c" |
|
807 by (metis assms(2) c d dividesI' prime_divides) |
|
808 with \<open>b = (p [^] n) \<otimes> c\<close> show ?case |
|
809 using assms(1) c by simp |
|
810 qed |
781 qed |
811 qed |
782 |
812 |
783 |
813 |
784 subsection \<open>Factorization and Factorial Monoids\<close> |
814 subsection \<open>Factorization and Factorial Monoids\<close> |
785 |
815 |