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