src/HOL/Library/Fundamental_Theorem_Algebra.thy
 changeset 55734 3f5b2745d659 parent 55358 85d81bc281d0 child 55735 81ba62493610
```     1.1 --- a/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Feb 25 15:02:54 2014 +0100
1.2 +++ b/src/HOL/Library/Fundamental_Theorem_Algebra.thy	Tue Feb 25 16:17:20 2014 +0000
1.3 @@ -7,6 +7,7 @@
1.4  begin
1.5
1.6  subsection {* Square root of complex numbers *}
1.7 +
1.8  definition csqrt :: "complex \<Rightarrow> complex" where
1.9  "csqrt z = (if Im z = 0 then
1.10              if 0 \<le> Re z then Complex (sqrt(Re z)) 0
1.11 @@ -54,6 +55,39 @@
1.12    ultimately show ?thesis by blast
1.13  qed
1.14
1.15 +lemma csqrt_Complex: "x \<ge> 0 \<Longrightarrow> csqrt (Complex x 0) = Complex (sqrt x) 0"
1.16 +  by (simp add: csqrt_def)
1.17 +
1.18 +lemma csqrt_0 [simp]: "csqrt 0 = 0"
1.19 +  by (simp add: csqrt_def)
1.20 +
1.21 +lemma csqrt_1 [simp]: "csqrt 1 = 1"
1.22 +  by (simp add: csqrt_def)
1.23 +
1.24 +lemma csqrt_principal: "0 < Re(csqrt(z)) | Re(csqrt(z)) = 0 & 0 \<le> Im(csqrt(z))"
1.25 +proof (cases z)
1.26 +  case (Complex x y)
1.27 +  then show ?thesis
1.28 +    using real_sqrt_sum_squares_ge1 [of "x" y]
1.29 +          real_sqrt_sum_squares_ge1 [of "-x" y]
1.30 +          real_sqrt_sum_squares_eq_cancel [of x y]
1.31 +    apply (auto simp: csqrt_def intro!: Rings.ordered_ring_class.split_mult_pos_le)
1.33 +    by (metis add_commute less_eq_real_def power_minus_Bit0 real_0_less_add_iff real_sqrt_sum_squares_eq_cancel)
1.34 +qed
1.35 +
1.36 +lemma Re_csqrt: "0 \<le> Re(csqrt z)"
1.37 +  by (metis csqrt_principal le_less)
1.38 +
1.39 +lemma csqrt_square: "(0 < Re z | Re z = 0 & 0 \<le> Im z) \<Longrightarrow> csqrt (z^2) = z"
1.40 +  using csqrt [of "z^2"] csqrt_principal [of "z^2"]
1.41 +  by (cases z) (auto simp: power2_eq_iff)
1.42 +
1.43 +lemma csqrt_eq_0 [simp]: "csqrt z = 0 \<longleftrightarrow> z = 0"
1.44 +  by auto (metis csqrt power_eq_0_iff)
1.45 +
1.46 +lemma csqrt_eq_1 [simp]: "csqrt z = 1 \<longleftrightarrow> z = 1"
1.47 +  by auto (metis csqrt power2_eq_1_iff)
1.48
1.49  subsection{* More lemmas about module of complex numbers *}
1.50
```