summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/GCD.thy

changeset 66936 | cf8d8fc23891 |

parent 66836 | 4eb431c3f974 |

child 67051 | e7e54a0b9197 |

1.1 --- a/src/HOL/GCD.thy Sun Oct 29 19:39:03 2017 +0100 1.2 +++ b/src/HOL/GCD.thy Mon Oct 30 13:18:41 2017 +0000 1.3 @@ -1600,13 +1600,10 @@ 1.4 by simp 1.5 next 1.6 case False 1.7 - then have "inj (times b)" 1.8 - by (rule inj_times) 1.9 show ?thesis proof (cases "finite A") 1.10 case False 1.11 - moreover from \<open>inj (times b)\<close> 1.12 - have "inj_on (times b) A" 1.13 - by (rule inj_on_subset) simp 1.14 + moreover have "inj_on (times b) A" 1.15 + using \<open>b \<noteq> 0\<close> by (rule inj_on_mult) 1.16 ultimately have "infinite (times b ` A)" 1.17 by (simp add: finite_image_iff) 1.18 with False show ?thesis