equal
deleted
inserted
replaced
3633 add: fps_const_add [symmetric] fps_const_neg [symmetric] |
3633 add: fps_const_add [symmetric] fps_const_neg [symmetric] |
3634 fps_sin_deriv fps_cos_deriv algebra_simps) |
3634 fps_sin_deriv fps_cos_deriv algebra_simps) |
3635 done |
3635 done |
3636 |
3636 |
3637 lemma fps_sin_even: "fps_sin (- c) = - fps_sin c" |
3637 lemma fps_sin_even: "fps_sin (- c) = - fps_sin c" |
3638 by (auto simp add: divide_minus_left fps_eq_iff fps_sin_def) |
3638 by (auto simp add: fps_eq_iff fps_sin_def) |
3639 |
3639 |
3640 lemma fps_cos_odd: "fps_cos (- c) = fps_cos c" |
3640 lemma fps_cos_odd: "fps_cos (- c) = fps_cos c" |
3641 by (auto simp add: fps_eq_iff fps_cos_def) |
3641 by (auto simp add: fps_eq_iff fps_cos_def) |
3642 |
3642 |
3643 definition "fps_tan c = fps_sin c / fps_cos c" |
3643 definition "fps_tan c = fps_sin c / fps_cos c" |