equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 header{*Fundamental Theorem of Algebra*} |
6 header{*Fundamental Theorem of Algebra*} |
7 |
7 |
8 theory Fundamental_Theorem_Algebra |
8 theory Fundamental_Theorem_Algebra |
9 imports Univ_Poly Dense_Linear_Order Complex |
9 imports "~~/src/HOL/Library/Univ_Poly" "~~/src/HOL/Library/Dense_Linear_Order" Complex |
10 begin |
10 begin |
11 |
11 |
12 subsection {* Square root of complex numbers *} |
12 subsection {* Square root of complex numbers *} |
13 definition csqrt :: "complex \<Rightarrow> complex" where |
13 definition csqrt :: "complex \<Rightarrow> complex" where |
14 "csqrt z = (if Im z = 0 then |
14 "csqrt z = (if Im z = 0 then |