src/HOL/Computational_Algebra/Euclidean_Algorithm.thy
changeset 67167 88d1c9d86f48
parent 66817 0b12755ccbb2
child 67399 eab6ce8368fa
     1.1 --- a/src/HOL/Computational_Algebra/Euclidean_Algorithm.thy	Mon Dec 11 17:28:32 2017 +0100
     1.2 +++ b/src/HOL/Computational_Algebra/Euclidean_Algorithm.thy	Tue Dec 12 10:01:14 2017 +0100
     1.3 @@ -602,6 +602,9 @@
     1.4      by (simp add: fun_eq_iff Euclidean_Algorithm.Gcd_def semiring_Gcd_class.Gcd_Lcm)
     1.5  qed
     1.6  
     1.7 +lemma prime_factorization_Suc_0 [simp]: "prime_factorization (Suc 0) = {#}"
     1.8 +  unfolding One_nat_def [symmetric] using prime_factorization_1 .
     1.9 +
    1.10  instance int :: normalization_euclidean_semiring ..
    1.11  
    1.12  instance int :: euclidean_ring_gcd