matita/contribs/CoRN-Decl/algebra/CPoly_ApZero.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/algebra/CPoly_ApZero".
  18
  19 (* $Id: CPoly_ApZero.v,v 1.3 2004/04/23 10:00:53 lcf Exp $ *)
  20
  21 (* INCLUDE
  22 CPoly_Degree
  23 *)
  24
  25 (* INCLUDE
  26 COrdFields2
  27 *)
  28
  29 (*#* * Polynomials apart from zero *)
  30
  31 inline cic:/CoRN/algebra/CPoly_ApZero/distinct1.con.
  32
  33 (* UNEXPORTED
  34 Implicit Arguments distinct1 [A].
  35 *)
  36
  37 (* UNEXPORTED
  38 Section Poly_Representation.
  39 *)
  40
  41 (*#*
  42 ** Representation of polynomials
  43 %\begin{convention}% Let [R] be a field, [RX] the ring of polynomials
  44 over [R], [a_ : nat->R] with [(distinct1 a_)] and let [f] be a
  45 polynomial over [R], [n] a natural with [(degree_le n f)], i.e. [f]
  46 has degree at most [n].
  47 %\end{convention}%
  48 *)
  49
  50 inline cic:/CoRN/algebra/CPoly_ApZero/R.var.
  51
  52 inline cic:/CoRN/algebra/CPoly_ApZero/a_.var.
  53
  54 inline cic:/CoRN/algebra/CPoly_ApZero/distinct_a_.var.
  55
  56 inline cic:/CoRN/algebra/CPoly_ApZero/f.var.
  57
  58 inline cic:/CoRN/algebra/CPoly_ApZero/n.var.
  59
  60 inline cic:/CoRN/algebra/CPoly_ApZero/degree_f.var.
  61
  62 (* begin hide *)
  63
  64 (* end hide *)
  65
  66 (* INCLUDE
  67 Transparent_algebra
  68 *)
  69
  70 inline cic:/CoRN/algebra/CPoly_ApZero/poly_linear_shifted.con.
  71
  72 (* INCLUDE
  73 Opaque_algebra
  74 *)
  75
  76 inline cic:/CoRN/algebra/CPoly_ApZero/poly_linear_factor.con.
  77
  78 inline cic:/CoRN/algebra/CPoly_ApZero/zero_poly.con.
  79
  80 inline cic:/CoRN/algebra/CPoly_ApZero/identical_poly.con.
  81
  82 inline cic:/CoRN/algebra/CPoly_ApZero/poly_01_factor'.con.
  83
  84 inline cic:/CoRN/algebra/CPoly_ApZero/poly_01_factor'_degree.con.
  85
  86 inline cic:/CoRN/algebra/CPoly_ApZero/poly_01_factor'_zero.con.
  87
  88 inline cic:/CoRN/algebra/CPoly_ApZero/poly_01_factor'_apzero.con.
  89
  90 (* UNEXPORTED
  91 Hint Resolve poly_01_factor'_zero.
  92 *)
  93
  94 inline cic:/CoRN/algebra/CPoly_ApZero/poly_01_factor.con.
  95
  96 inline cic:/CoRN/algebra/CPoly_ApZero/poly_01_factor_degree.con.
  97
  98 inline cic:/CoRN/algebra/CPoly_ApZero/poly_01_factor_zero.con.
  99
 100 inline cic:/CoRN/algebra/CPoly_ApZero/poly_01_factor_one.con.
 101
 102 (* UNEXPORTED
 103 Hint Resolve poly_01_factor_zero poly_01_factor_one: algebra.
 104 *)
 105
 106 inline cic:/CoRN/algebra/CPoly_ApZero/poly_01.con.
 107
 108 inline cic:/CoRN/algebra/CPoly_ApZero/poly_01_degree'.con.
 109
 110 inline cic:/CoRN/algebra/CPoly_ApZero/poly_01_degree.con.
 111
 112 inline cic:/CoRN/algebra/CPoly_ApZero/poly_01_zero.con.
 113
 114 inline cic:/CoRN/algebra/CPoly_ApZero/poly_01_one.con.
 115
 116 (* UNEXPORTED
 117 Hint Resolve poly_01_zero poly_01_one: algebra.
 118 *)
 119
 120 inline cic:/CoRN/algebra/CPoly_ApZero/poly_representation''.con.
 121
 122 inline cic:/CoRN/algebra/CPoly_ApZero/poly_representation'.con.
 123
 124 inline cic:/CoRN/algebra/CPoly_ApZero/poly_representation.con.
 125
 126 (* UNEXPORTED
 127 Hint Resolve poly_representation: algebra.
 128 *)
 129
 130 inline cic:/CoRN/algebra/CPoly_ApZero/Cpoly_choose_apzero.con.
 131
 132 (* UNEXPORTED
 133 End Poly_Representation.
 134 *)
 135
 136 (* UNEXPORTED
 137 Section Characteristic_zero.
 138 *)
 139
 140 (*#*
 141 If we are in a field of characteristic zero, the previous result can be
 142 strengthened.
 143 *)
 144
 145 inline cic:/CoRN/algebra/CPoly_ApZero/R.var.
 146
 147 (* begin show *)
 148
 149 inline cic:/CoRN/algebra/CPoly_ApZero/H.var.
 150
 151 (* end show *)
 152
 153 (* begin hide *)
 154
 155 (* end hide *)
 156
 157 inline cic:/CoRN/algebra/CPoly_ApZero/poly_apzero.con.
 158
 159 (*#*
 160 Also, in this situation polynomials are extensional functions.
 161 *)
 162
 163 inline cic:/CoRN/algebra/CPoly_ApZero/poly_extensional.con.
 164
 165 (* UNEXPORTED
 166 End Characteristic_zero.
 167 *)
 168
 169 (*#*
 170 ** Polynomials are nonzero on any interval
 171 *)
 172
 173 (* UNEXPORTED
 174 Section Poly_ApZero_Interval.
 175 *)
 176
 177 inline cic:/CoRN/algebra/CPoly_ApZero/R.var.
 178
 179 (* begin hide *)
 180
 181 (* end hide *)
 182
 183 inline cic:/CoRN/algebra/CPoly_ApZero/Cpoly_apzero_interval.con.
 184
 185 (* UNEXPORTED
 186 End Poly_ApZero_Interval.
 187 *)
 188