]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/CoRN-Decl/fta/FTA.ma
- uniform relocations
[helm.git] / matita / matita / contribs / CoRN-Decl / fta / FTA.ma
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 set "baseuri" "cic:/matita/CoRN-Decl/fta/FTA".
18
19 include "CoRN.ma".
20
21 (* $Id: FTA.v,v 1.6 2004/04/23 10:00:57 lcf Exp $ *)
22
23 include "fta/CPoly_Rev.ma".
24
25 include "fta/FTAreg.ma".
26
27 (*#* * Fundamental Theorem of Algebra
28 %\begin{convention}% Let [n:nat] and [f] be a complex polynomial of
29 degree [(S n)].
30 %\end{convention}%
31 *)
32
33 (* UNEXPORTED
34 Section FTA_reg'
35 *)
36
37 alias id "f" = "cic:/CoRN/fta/FTA/FTA_reg'/f.var".
38
39 alias id "n" = "cic:/CoRN/fta/FTA/FTA_reg'/n.var".
40
41 alias id "f_degree" = "cic:/CoRN/fta/FTA/FTA_reg'/f_degree.var".
42
43 inline "cic:/CoRN/fta/FTA/FTA_reg'.con".
44
45 (* UNEXPORTED
46 End FTA_reg'
47 *)
48
49 (*#*
50 %\begin{convention}% Let [n:nat], [f] be a complex polynomial of degree
51 less than or equal to [(S n)] and [c] be a complex number such that
52 [f!c  [#]  Zero].
53 %\end{convention}%
54 *)
55
56 (* UNEXPORTED
57 Section FTA_1
58 *)
59
60 alias id "f" = "cic:/CoRN/fta/FTA/FTA_1/f.var".
61
62 alias id "n" = "cic:/CoRN/fta/FTA/FTA_1/n.var".
63
64 alias id "f_degree" = "cic:/CoRN/fta/FTA/FTA_1/f_degree.var".
65
66 alias id "c" = "cic:/CoRN/fta/FTA/FTA_1/c.var".
67
68 alias id "f_c" = "cic:/CoRN/fta/FTA/FTA_1/f_c.var".
69
70 inline "cic:/CoRN/fta/FTA/FTA_1a.con".
71
72 inline "cic:/CoRN/fta/FTA/FTA_1/g.con" "FTA_1__".
73
74 inline "cic:/CoRN/fta/FTA/FTA_1b.con".
75
76 inline "cic:/CoRN/fta/FTA/FTA_1.con".
77
78 inline "cic:/CoRN/fta/FTA/FTA_1'.con".
79
80 (* UNEXPORTED
81 End FTA_1
82 *)
83
84 (* UNEXPORTED
85 Section Fund_Thm_Alg
86 *)
87
88 inline "cic:/CoRN/fta/FTA/FTA'.con".
89
90 inline "cic:/CoRN/fta/FTA/FTA.con".
91
92 inline "cic:/CoRN/fta/FTA/FTA_a_la_Henk.con".
93
94 (* UNEXPORTED
95 End Fund_Thm_Alg
96 *)
97