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