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