equal
deleted
inserted
replaced
1025 lemma rcis_cmod_arg: "rcis (cmod z) (arg z) = z" |
1025 lemma rcis_cmod_arg: "rcis (cmod z) (arg z) = z" |
1026 by (cases "z = 0") (simp_all add: rcis_def cis_arg sgn_div_norm of_real_def) |
1026 by (cases "z = 0") (simp_all add: rcis_def cis_arg sgn_div_norm of_real_def) |
1027 |
1027 |
1028 lemma cos_arg_i_mult_zero [simp]: "y \<noteq> 0 \<Longrightarrow> Re y = 0 \<Longrightarrow> cos (arg y) = 0" |
1028 lemma cos_arg_i_mult_zero [simp]: "y \<noteq> 0 \<Longrightarrow> Re y = 0 \<Longrightarrow> cos (arg y) = 0" |
1029 using cis_arg [of y] by (simp add: complex_eq_iff) |
1029 using cis_arg [of y] by (simp add: complex_eq_iff) |
|
1030 |
|
1031 lemma arg_ii [simp]: "arg \<i> = pi/2" |
|
1032 by (rule arg_unique; simp add: sgn_eq) |
|
1033 |
|
1034 lemma arg_minus_ii [simp]: "arg (-\<i>) = -pi/2" |
|
1035 proof (rule arg_unique) |
|
1036 show "sgn (- \<i>) = cis (- pi / 2)" |
|
1037 by (simp add: sgn_eq) |
|
1038 show "- pi / 2 \<le> pi" |
|
1039 using pi_not_less_zero by linarith |
|
1040 qed auto |
1030 |
1041 |
1031 subsection \<open>Complex n-th roots\<close> |
1042 subsection \<open>Complex n-th roots\<close> |
1032 |
1043 |
1033 lemma bij_betw_roots_unity: |
1044 lemma bij_betw_roots_unity: |
1034 assumes "n > 0" |
1045 assumes "n > 0" |