equal
deleted
inserted
replaced
25 |
25 |
26 lemma fps_of_poly_0 [simp]: "fps_of_poly 0 = 0" |
26 lemma fps_of_poly_0 [simp]: "fps_of_poly 0 = 0" |
27 by (subst fps_const_0_eq_0 [symmetric], subst fps_of_poly_const [symmetric]) simp |
27 by (subst fps_const_0_eq_0 [symmetric], subst fps_of_poly_const [symmetric]) simp |
28 |
28 |
29 lemma fps_of_poly_1 [simp]: "fps_of_poly 1 = 1" |
29 lemma fps_of_poly_1 [simp]: "fps_of_poly 1 = 1" |
30 by (subst fps_const_1_eq_1 [symmetric], subst fps_of_poly_const [symmetric]) |
30 by (simp add: fps_eq_iff) |
31 (simp add: one_poly_def) |
|
32 |
31 |
33 lemma fps_of_poly_1' [simp]: "fps_of_poly [:1:] = 1" |
32 lemma fps_of_poly_1' [simp]: "fps_of_poly [:1:] = 1" |
34 by (subst fps_const_1_eq_1 [symmetric], subst fps_of_poly_const [symmetric]) |
33 by (subst fps_const_1_eq_1 [symmetric], subst fps_of_poly_const [symmetric]) |
35 (simp add: one_poly_def) |
34 (simp add: one_poly_def) |
36 |
35 |