]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/contribs/procedural/CoRN/fta/FTA.mma
transcript: we improved the parser/lexer to read the scripts of the standard
[helm.git] / helm / software / matita / contribs / procedural / CoRN / fta / FTA.mma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 (* This file was automatically generated: do not edit *********************)
16
17 include "CoRN.ma".
18
19 (* $Id: FTA.v,v 1.6 2004/04/23 10:00:57 lcf Exp $ *)
20
21 include "fta/CPoly_Rev.ma".
22
23 include "fta/FTAreg.ma".
24
25 (*#* * Fundamental Theorem of Algebra
26 %\begin{convention}% Let [n:nat] and [f] be a complex polynomial of
27 degree [(S n)].
28 %\end{convention}%
29 *)
30
31 (* UNEXPORTED
32 Section FTA_reg'
33 *)
34
35 (* UNEXPORTED
36 cic:/CoRN/fta/FTA/FTA_reg'/f.var
37 *)
38
39 (* UNEXPORTED
40 cic:/CoRN/fta/FTA/FTA_reg'/n.var
41 *)
42
43 (* UNEXPORTED
44 cic:/CoRN/fta/FTA/FTA_reg'/f_degree.var
45 *)
46
47 inline procedural "cic:/CoRN/fta/FTA/FTA_reg'.con" as lemma.
48
49 (* UNEXPORTED
50 End FTA_reg'
51 *)
52
53 (*#*
54 %\begin{convention}% Let [n:nat], [f] be a complex polynomial of degree
55 less than or equal to [(S n)] and [c] be a complex number such that
56 [f!c  [#]  Zero].
57 %\end{convention}%
58 *)
59
60 (* UNEXPORTED
61 Section FTA_1
62 *)
63
64 (* UNEXPORTED
65 cic:/CoRN/fta/FTA/FTA_1/f.var
66 *)
67
68 (* UNEXPORTED
69 cic:/CoRN/fta/FTA/FTA_1/n.var
70 *)
71
72 (* UNEXPORTED
73 cic:/CoRN/fta/FTA/FTA_1/f_degree.var
74 *)
75
76 (* UNEXPORTED
77 cic:/CoRN/fta/FTA/FTA_1/c.var
78 *)
79
80 (* UNEXPORTED
81 cic:/CoRN/fta/FTA/FTA_1/f_c.var
82 *)
83
84 inline procedural "cic:/CoRN/fta/FTA/FTA_1a.con" as lemma.
85
86 inline procedural "cic:/CoRN/fta/FTA/FTA_1/g.con" "FTA_1__" as definition.
87
88 inline procedural "cic:/CoRN/fta/FTA/FTA_1b.con" as lemma.
89
90 inline procedural "cic:/CoRN/fta/FTA/FTA_1.con" as lemma.
91
92 inline procedural "cic:/CoRN/fta/FTA/FTA_1'.con" as lemma.
93
94 (* UNEXPORTED
95 End FTA_1
96 *)
97
98 (* UNEXPORTED
99 Section Fund_Thm_Alg
100 *)
101
102 inline procedural "cic:/CoRN/fta/FTA/FTA'.con" as lemma.
103
104 inline procedural "cic:/CoRN/fta/FTA/FTA.con" as lemma.
105
106 inline procedural "cic:/CoRN/fta/FTA/FTA_a_la_Henk.con" as lemma.
107
108 (* UNEXPORTED
109 End Fund_Thm_Alg
110 *)
111