equal
deleted
inserted
replaced
255 apply (unfold Let_def, auto) |
255 apply (unfold Let_def, auto) |
256 apply (simp add: Bnor_fin Bnor_mem_zle_swap) |
256 apply (simp add: Bnor_fin Bnor_mem_zle_swap) |
257 apply (subst setprod_insert) |
257 apply (subst setprod_insert) |
258 apply (rule_tac [2] Bnor_prod_power_aux) |
258 apply (rule_tac [2] Bnor_prod_power_aux) |
259 apply (unfold inj_on_def) |
259 apply (unfold inj_on_def) |
260 apply (simp_all add: zmult_ac Bnor_fin finite_imageI |
260 apply (simp_all add: zmult_ac Bnor_fin Bnor_mem_zle_swap) |
261 Bnor_mem_zle_swap) |
|
262 done |
261 done |
263 |
262 |
264 |
263 |
265 subsection {* Fermat *} |
264 subsection {* Fermat *} |
266 |
265 |