# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# Date 1614178156 0
# Node ID 915b3d41dec104c30f6c7c806617f5ffd19de6ac
# Parent  f5a77ee9106cd14a0c5992aa10bf7ab50c16cbbf
A couple of basic lemmas about arg

diff -r f5a77ee9106c -r 915b3d41dec1 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Sun Feb 21 13:33:05 2021 +0100
+++ b/src/HOL/Complex.thy	Wed Feb 24 14:49:16 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: