# HG changeset patch
# User haftmann
# Date 1614256554 -3600
# Node ID 95937cfe2628ac445701d25098ac11b24e8b7644
# Parent  47616dc81488df7d28c525a18f3f92d3345ac78b# Parent  6cd53ec2e32e38356372d836626b38ab706d603b
merged

diff -r 47616dc81488 -r 95937cfe2628 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Wed Feb 24 21:45:09 2021 +0100
+++ b/src/HOL/Complex.thy	Thu Feb 25 13:35:54 2021 +0100
@@ -1028,6 +1028,17 @@
 lemma cos_arg_i_mult_zero [simp]: "y \<noteq> 0 \<Longrightarrow> Re y = 0 \<Longrightarrow> cos (arg y) = 0"
   using cis_arg [of y] by (simp add: complex_eq_iff)
 
+lemma arg_ii [simp]: "arg \<i> = pi/2"
+  by (rule arg_unique; simp add: sgn_eq)
+
+lemma arg_minus_ii [simp]: "arg (-\<i>) = -pi/2"
+proof (rule arg_unique)
+  show "sgn (- \<i>) = cis (- pi / 2)"
+    by (simp add: sgn_eq)
+  show "- pi / 2 \<le> pi"
+    using pi_not_less_zero by linarith
+qed auto
+
 subsection \<open>Complex n-th roots\<close>
 
 lemma bij_betw_roots_unity: