equal
deleted
inserted
replaced
1598 by auto |
1598 by auto |
1599 ultimately show ?thesis |
1599 ultimately show ?thesis |
1600 by simp |
1600 by simp |
1601 next |
1601 next |
1602 case False |
1602 case False |
1603 then have "inj (times b)" |
|
1604 by (rule inj_times) |
|
1605 show ?thesis proof (cases "finite A") |
1603 show ?thesis proof (cases "finite A") |
1606 case False |
1604 case False |
1607 moreover from \<open>inj (times b)\<close> |
1605 moreover have "inj_on (times b) A" |
1608 have "inj_on (times b) A" |
1606 using \<open>b \<noteq> 0\<close> by (rule inj_on_mult) |
1609 by (rule inj_on_subset) simp |
|
1610 ultimately have "infinite (times b ` A)" |
1607 ultimately have "infinite (times b ` A)" |
1611 by (simp add: finite_image_iff) |
1608 by (simp add: finite_image_iff) |
1612 with False show ?thesis |
1609 with False show ?thesis |
1613 by simp |
1610 by simp |
1614 next |
1611 next |