equal
deleted
inserted
replaced
4531 del: fps_const_neg) |
4531 del: fps_const_neg) |
4532 also note fps_sin_cos_sum_of_squares |
4532 also note fps_sin_cos_sum_of_squares |
4533 finally show ?thesis by simp |
4533 finally show ?thesis by simp |
4534 qed |
4534 qed |
4535 |
4535 |
4536 text \<open>Connection to @{const "fps_exp"} over the complex numbers --- Euler and de Moivre.\<close> |
4536 text \<open>Connection to \<^const>\<open>fps_exp\<close> over the complex numbers --- Euler and de Moivre.\<close> |
4537 |
4537 |
4538 lemma fps_exp_ii_sin_cos: "fps_exp (\<i> * c) = fps_cos c + fps_const \<i> * fps_sin c" |
4538 lemma fps_exp_ii_sin_cos: "fps_exp (\<i> * c) = fps_cos c + fps_const \<i> * fps_sin c" |
4539 (is "?l = ?r") |
4539 (is "?l = ?r") |
4540 proof - |
4540 proof - |
4541 have "?l $ n = ?r $ n" for n |
4541 have "?l $ n = ?r $ n" for n |