equal
deleted
inserted
replaced
671 done |
671 done |
672 qed |
672 qed |
673 |
673 |
674 subsection\<open>Polar Form for Complex Numbers\<close> |
674 subsection\<open>Polar Form for Complex Numbers\<close> |
675 |
675 |
676 lemma complex_unimodular_polar: "(norm z = 1) \<Longrightarrow> \<exists>x. z = Complex (cos x) (sin x)" |
676 lemma complex_unimodular_polar: |
677 using sincos_total_2pi [of "Re z" "Im z"] |
677 assumes "(norm z = 1)" |
678 by auto (metis cmod_power2 complex_eq power_one) |
678 obtains t where "0 \<le> t" "t < 2*pi" "z = Complex (cos t) (sin t)" |
|
679 by (metis cmod_power2 one_power2 complex_surj sincos_total_2pi [of "Re z" "Im z"] assms) |
679 |
680 |
680 subsubsection \<open>$\cos \theta + i \sin \theta$\<close> |
681 subsubsection \<open>$\cos \theta + i \sin \theta$\<close> |
681 |
682 |
682 primcorec cis :: "real \<Rightarrow> complex" where |
683 primcorec cis :: "real \<Rightarrow> complex" where |
683 "Re (cis a) = cos a" |
684 "Re (cis a) = cos a" |