equal
deleted
inserted
replaced
214 using assms is_cring by (auto simp add: cgenideal_ideal) |
214 using assms is_cring by (auto simp add: cgenideal_ideal) |
215 show "carrier R \<noteq> PIdl p" |
215 show "carrier R \<noteq> PIdl p" |
216 proof (rule ccontr) |
216 proof (rule ccontr) |
217 assume "\<not> carrier R \<noteq> PIdl p" hence "carrier R = PIdl p" by simp |
217 assume "\<not> carrier R \<noteq> PIdl p" hence "carrier R = PIdl p" by simp |
218 then obtain c where "c \<in> carrier R" "c \<otimes> p = \<one>" |
218 then obtain c where "c \<in> carrier R" "c \<otimes> p = \<one>" |
219 unfolding cgenideal_def using one_closed by (smt mem_Collect_eq) |
219 unfolding cginideal_def' by (metis (no_types, lifting) image_iff one_closed) |
220 hence "p \<in> Units R" unfolding Units_def using m_comm assms by auto |
220 hence "p \<in> Units R" unfolding Units_def using m_comm assms by auto |
221 thus False using A unfolding prime_def by simp |
221 thus False using A unfolding prime_def by simp |
222 qed |
222 qed |
223 fix a b assume a: "a \<in> carrier R" and b: "b \<in> carrier R" and ab: "a \<otimes> b \<in> PIdl p" |
223 fix a b assume a: "a \<in> carrier R" and b: "b \<in> carrier R" and ab: "a \<otimes> b \<in> PIdl p" |
224 thus "a \<in> PIdl p \<or> b \<in> PIdl p" |
224 thus "a \<in> PIdl p \<or> b \<in> PIdl p" |