114 proof - |
114 proof - |
115 from assms have nz: "a * b \<noteq> 0" by auto |
115 from assms have nz: "a * b \<noteq> 0" by auto |
116 show ?thesis unfolding squarefree_factorial_semiring'[OF nz] |
116 show ?thesis unfolding squarefree_factorial_semiring'[OF nz] |
117 proof |
117 proof |
118 fix p assume p: "p \<in> prime_factors (a * b)" |
118 fix p assume p: "p \<in> prime_factors (a * b)" |
119 { |
119 with nz have "prime p" |
|
120 by (simp add: prime_factors_dvd) |
|
121 have "\<not> (p dvd a \<and> p dvd b)" |
|
122 proof |
120 assume "p dvd a \<and> p dvd b" |
123 assume "p dvd a \<and> p dvd b" |
121 hence "p dvd gcd a b" by simp |
124 with \<open>coprime a b\<close> have "is_unit p" |
122 also have "gcd a b = 1" by fact |
125 by (auto intro: coprime_common_divisor) |
123 finally have False using nz using p by (auto simp: prime_factors_dvd) |
126 with \<open>prime p\<close> show False |
124 } |
127 by simp |
125 hence "\<not>(p dvd a \<and> p dvd b)" by blast |
128 qed |
126 moreover from p have "p dvd a \<or> p dvd b" using nz |
129 moreover from p have "p dvd a \<or> p dvd b" using nz |
127 by (auto simp: prime_factors_dvd prime_dvd_mult_iff) |
130 by (auto simp: prime_factors_dvd prime_dvd_mult_iff) |
128 ultimately show "multiplicity p (a * b) = 1" using nz p assms(2,3) |
131 ultimately show "multiplicity p (a * b) = 1" using nz p assms(2,3) |
129 by (auto simp: prime_elem_multiplicity_mult_distrib prime_factors_multiplicity |
132 by (auto simp: prime_elem_multiplicity_mult_distrib prime_factors_multiplicity |
130 not_dvd_imp_multiplicity_0 squarefree_factorial_semiring') |
133 not_dvd_imp_multiplicity_0 squarefree_factorial_semiring') |
136 assumes "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> coprime (f a) (f b)" |
139 assumes "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> coprime (f a) (f b)" |
137 assumes "\<And>a. a \<in> A \<Longrightarrow> squarefree (f a)" |
140 assumes "\<And>a. a \<in> A \<Longrightarrow> squarefree (f a)" |
138 shows "squarefree (prod f A)" |
141 shows "squarefree (prod f A)" |
139 using assms |
142 using assms |
140 by (induction A rule: infinite_finite_induct) |
143 by (induction A rule: infinite_finite_induct) |
141 (auto intro!: squarefree_mult_coprime prod_coprime') |
144 (auto intro!: squarefree_mult_coprime prod_coprime_right) |
142 |
145 |
143 lemma squarefree_powerD: "m > 0 \<Longrightarrow> squarefree (n ^ m) \<Longrightarrow> squarefree n" |
146 lemma squarefree_powerD: "m > 0 \<Longrightarrow> squarefree (n ^ m) \<Longrightarrow> squarefree n" |
144 by (cases m) (auto dest: squarefree_multD) |
147 by (cases m) (auto dest: squarefree_multD) |
145 |
148 |
146 lemma squarefree_power_iff: |
149 lemma squarefree_power_iff: |