src/HOL/Complex/Fundamental_Theorem_Algebra.thy

 
 theory Fundamental_Theorem_Algebra
 imports Univ_Poly Dense_Linear_Order Complex
 begin
 
-section {* Square root of complex numbers *}
+subsection {* Square root of complex numbers *}
 definition csqrt :: "complex \<Rightarrow> complex" where
 "csqrt z = (if Im z = 0 then
             if 0 \<le> Re z then Complex (sqrt(Re z)) 0
             else Complex 0 (sqrt(- Re z))
            else Complex (sqrt((cmod z + Re z) /2))

       using th1 th2  ..}
   ultimately show ?thesis by blast
 qed
 
 
-section{* More lemmas about module of complex numbers *}
+subsection{* More lemmas about module of complex numbers *}
 
 lemma complex_of_real_power: "complex_of_real x ^ n = complex_of_real (x^n)"
   by (induct n, auto)
 
 lemma cmod_pos: "cmod z \<ge> 0" by simp

 
 text{* The triangle inequality for cmod *}
 lemma complex_mod_triangle_sub: "cmod w \<le> cmod (w + z) + norm z"
   using complex_mod_triangle_ineq2[of "w + z" "-z"] by auto
 
-section{* Basic lemmas about complex polynomials *}
+subsection{* Basic lemmas about complex polynomials *}
 
 lemma poly_bound_exists:
   shows "\<exists>m. m > 0 \<and> (\<forall>z. cmod z <= r \<longrightarrow> cmod (poly p z) \<le> m)"
 proof(induct p)
   case Nil thus ?case by (rule exI[where x=1], simp) 

     ultimately have "(\<exists>x. P x \<and> y < x) \<longleftrightarrow> y < L" by blast}
   thus ?thesis by blast
 qed
 
 
-section{* Some theorems about Sequences*}
+subsection{* Some theorems about Sequences*}
 text{* Given a binary function @{text "f:: nat \<Rightarrow> 'a \<Rightarrow> 'a"}, its values are uniquely determined by a function g *}
 
 lemma num_Axiom: "EX! g. g 0 = e \<and> (\<forall>n. g (Suc n) = f n (g n))"
   unfolding Ex1_def
   apply (rule_tac x="nat_rec e f" in exI)

   from sf[unfolded subseq_Suc_iff, rule_format, of n] Suc.hyps
   have "n < f (Suc n)" by arith 
   thus ?case by arith
 qed
 
-section {* Fundamental theorem of algebra *}
+subsection {* Fundamental theorem of algebra *}
 lemma  unimodular_reduce_norm:
   assumes md: "cmod z = 1"
   shows "cmod (z + 1) < 1 \<or> cmod (z - 1) < 1 \<or> cmod (z + ii) < 1 \<or> cmod (z - ii) < 1"
 proof-
   obtain x y where z: "z = Complex x y " by (cases z, auto)

 	by blast
       from fundamental_theorem_of_algebra[OF nc] have ?case .}
   ultimately show ?case by blast  
 qed simp
 
-section{* Nullstellenstatz, degrees and divisibility of polynomials *}
+subsection{* Nullstellenstatz, degrees and divisibility of polynomials *}
 
 lemma nullstellensatz_lemma:
   fixes p :: "complex list"
   assumes "\<forall>x. poly p x = 0 \<longrightarrow> poly q x = 0"
   and "degree p = n" and "n \<noteq> 0"