equal
deleted
inserted
replaced
2303 case (Suc n) |
2303 case (Suc n) |
2304 then have c: "m = card {0..n}" by simp |
2304 then have c: "m = card {0..n}" by simp |
2305 have "(a ^m)$0 = setprod (\<lambda>i. a$0) {0..n}" |
2305 have "(a ^m)$0 = setprod (\<lambda>i. a$0) {0..n}" |
2306 by (simp add: Suc fps_power_nth del: replicate.simps power_Suc) |
2306 by (simp add: Suc fps_power_nth del: replicate.simps power_Suc) |
2307 also have "\<dots> = (a$0) ^ m" |
2307 also have "\<dots> = (a$0) ^ m" |
2308 unfolding c by (rule setprod_constant) simp |
2308 unfolding c by (rule setprod_constant) |
2309 finally show ?thesis . |
2309 finally show ?thesis . |
2310 qed |
2310 qed |
2311 |
2311 |
2312 lemma fps_compose_inj_right: |
2312 lemma fps_compose_inj_right: |
2313 assumes a0: "a$0 = (0::'a::idom)" |
2313 assumes a0: "a$0 = (0::'a::idom)" |