author huffman Wed, 02 Jul 2008 19:52:57 +0200 changeset 27445 0829a2c4b287 parent 27444 a487aa892540 child 27446 bac210482607
section -> subsection
```--- a/src/HOL/Complex/Fundamental_Theorem_Algebra.thy	Wed Jul 02 19:52:38 2008 +0200
+++ b/src/HOL/Complex/Fundamental_Theorem_Algebra.thy	Wed Jul 02 19:52:57 2008 +0200
@@ -9,7 +9,7 @@
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
@@ -56,7 +56,7 @@
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)
@@ -108,7 +108,7 @@
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)"
@@ -196,7 +196,7 @@
qed

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))"
@@ -360,7 +360,7 @@
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"
@@ -984,7 +984,7 @@
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"```