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