src/HOL/Algebra/Divisibility.thy
 changeset 68551 b680e74eb6f2 parent 68488 dfbd80c3d180 child 68604 57721285d4ef
```     1.1 --- a/src/HOL/Algebra/Divisibility.thy	Fri Jun 29 23:04:36 2018 +0200
1.2 +++ b/src/HOL/Algebra/Divisibility.thy	Sat Jun 30 15:44:04 2018 +0100
1.3 @@ -763,6 +763,27 @@
1.4    apply (metis pp' associated_sym divides_cong_l)
1.5    done
1.6
1.7 +(*by Paulo EmÃ­lio de Vilhena*)
1.8 +lemma (in comm_monoid_cancel) prime_irreducible:
1.9 +  assumes "prime G p"
1.10 +  shows "irreducible G p"
1.11 +proof (rule irreducibleI)
1.12 +  show "p \<notin> Units G"
1.13 +    using assms unfolding prime_def by simp
1.14 +next
1.15 +  fix b assume A: "b \<in> carrier G" "properfactor G b p"
1.16 +  then obtain c where c: "c \<in> carrier G" "p = b \<otimes> c"
1.17 +    unfolding properfactor_def factor_def by auto
1.18 +  hence "p divides c"
1.19 +    using A assms unfolding prime_def properfactor_def by auto
1.20 +  then obtain b' where b': "b' \<in> carrier G" "c = p \<otimes> b'"
1.21 +    unfolding factor_def by auto
1.22 +  hence "\<one> = b \<otimes> b'"
1.23 +    by (metis A(1) l_cancel m_closed m_lcomm one_closed r_one c)
1.24 +  thus "b \<in> Units G"
1.25 +    using A(1) Units_one_closed b'(1) unit_factor by presburger
1.26 +qed
1.27 +
1.28
1.29  subsection \<open>Factorization and Factorial Monoids\<close>
1.30
```