# HG changeset patch
# User paulson
# Date 1614192099 0
# Node ID 6cd53ec2e32e38356372d836626b38ab706d603b
# Parent  bfe92e4f6ea4c5883b8cd07e0292eb3e3b322c90# Parent  bd61e9477d82d93ef243b863c856a3c36b6a6418
merged

diff -r bfe92e4f6ea4 -r 6cd53ec2e32e src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Wed Feb 24 13:31:33 2021 +0000
+++ b/src/HOL/Complex.thy	Wed Feb 24 18:41:39 2021 +0000
@@ -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: