# HG changeset patch
# User paulson
# Date 1614178176 0
# Node ID bd61e9477d82d93ef243b863c856a3c36b6a6418
# Parent  637e3e85cd6fd61f7ac3d4000f753a93ef63edf3# Parent  915b3d41dec104c30f6c7c806617f5ffd19de6ac
merged

diff -r 637e3e85cd6f -r bd61e9477d82 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Tue Feb 23 23:00:08 2021 +0100
+++ b/src/HOL/Complex.thy	Wed Feb 24 14:49:36 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: