helm/software/matita/contribs/CoRN-Procedural/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".
  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 alias id "R" = "cic:/CoRN/algebra/CPoly_ApZero/Poly_Representation/R.var".
  47
  48 alias id "a_" = "cic:/CoRN/algebra/CPoly_ApZero/Poly_Representation/a_.var".
  49
  50 alias id "distinct_a_" = "cic:/CoRN/algebra/CPoly_ApZero/Poly_Representation/distinct_a_.var".
  51
  52 alias id "f" = "cic:/CoRN/algebra/CPoly_ApZero/Poly_Representation/f.var".
  53
  54 alias id "n" = "cic:/CoRN/algebra/CPoly_ApZero/Poly_Representation/n.var".
  55
  56 alias id "degree_f" = "cic:/CoRN/algebra/CPoly_ApZero/Poly_Representation/degree_f.var".
  57
  58 (* begin hide *)
  59
  60 (* NOTATION
  61 Notation RX := (cpoly_cring R).
  62 *)
  63
  64 (* end hide *)
  65
  66 include "tactics/Transparent_algebra.ma".
  67
  68 inline procedural "cic:/CoRN/algebra/CPoly_ApZero/poly_linear_shifted.con".
  69
  70 include "tactics/Opaque_algebra.ma".
  71
  72 inline procedural "cic:/CoRN/algebra/CPoly_ApZero/poly_linear_factor.con".
  73
  74 inline procedural "cic:/CoRN/algebra/CPoly_ApZero/zero_poly.con".
  75
  76 inline procedural "cic:/CoRN/algebra/CPoly_ApZero/identical_poly.con".
  77
  78 inline procedural "cic:/CoRN/algebra/CPoly_ApZero/poly_01_factor'.con".
  79
  80 inline procedural "cic:/CoRN/algebra/CPoly_ApZero/poly_01_factor'_degree.con".
  81
  82 inline procedural "cic:/CoRN/algebra/CPoly_ApZero/poly_01_factor'_zero.con".
  83
  84 inline procedural "cic:/CoRN/algebra/CPoly_ApZero/poly_01_factor'_apzero.con".
  85
  86 (* UNEXPORTED
  87 Hint Resolve poly_01_factor'_zero.
  88 *)
  89
  90 inline procedural "cic:/CoRN/algebra/CPoly_ApZero/poly_01_factor.con".
  91
  92 inline procedural "cic:/CoRN/algebra/CPoly_ApZero/poly_01_factor_degree.con".
  93
  94 inline procedural "cic:/CoRN/algebra/CPoly_ApZero/poly_01_factor_zero.con".
  95
  96 inline procedural "cic:/CoRN/algebra/CPoly_ApZero/poly_01_factor_one.con".
  97
  98 (* UNEXPORTED
  99 Hint Resolve poly_01_factor_zero poly_01_factor_one: algebra.
 100 *)
 101
 102 inline procedural "cic:/CoRN/algebra/CPoly_ApZero/poly_01.con".
 103
 104 inline procedural "cic:/CoRN/algebra/CPoly_ApZero/poly_01_degree'.con".
 105
 106 inline procedural "cic:/CoRN/algebra/CPoly_ApZero/poly_01_degree.con".
 107
 108 inline procedural "cic:/CoRN/algebra/CPoly_ApZero/poly_01_zero.con".
 109
 110 inline procedural "cic:/CoRN/algebra/CPoly_ApZero/poly_01_one.con".
 111
 112 (* UNEXPORTED
 113 Hint Resolve poly_01_zero poly_01_one: algebra.
 114 *)
 115
 116 inline procedural "cic:/CoRN/algebra/CPoly_ApZero/poly_representation''.con".
 117
 118 inline procedural "cic:/CoRN/algebra/CPoly_ApZero/poly_representation'.con".
 119
 120 inline procedural "cic:/CoRN/algebra/CPoly_ApZero/poly_representation.con".
 121
 122 (* UNEXPORTED
 123 Hint Resolve poly_representation: algebra.
 124 *)
 125
 126 inline procedural "cic:/CoRN/algebra/CPoly_ApZero/Cpoly_choose_apzero.con".
 127
 128 (* UNEXPORTED
 129 End Poly_Representation
 130 *)
 131
 132 (* UNEXPORTED
 133 Section Characteristic_zero
 134 *)
 135
 136 (*#*
 137 If we are in a field of characteristic zero, the previous result can be
 138 strengthened.
 139 *)
 140
 141 alias id "R" = "cic:/CoRN/algebra/CPoly_ApZero/Characteristic_zero/R.var".
 142
 143 (* begin show *)
 144
 145 alias id "H" = "cic:/CoRN/algebra/CPoly_ApZero/Characteristic_zero/H.var".
 146
 147 (* end show *)
 148
 149 (* begin hide *)
 150
 151 (* NOTATION
 152 Notation RX := (cpoly_cring R).
 153 *)
 154
 155 (* end hide *)
 156
 157 inline procedural "cic:/CoRN/algebra/CPoly_ApZero/poly_apzero.con".
 158
 159 (*#*
 160 Also, in this situation polynomials are extensional functions.
 161 *)
 162
 163 inline procedural "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 alias id "R" = "cic:/CoRN/algebra/CPoly_ApZero/Poly_ApZero_Interval/R.var".
 178
 179 (* begin hide *)
 180
 181 (* NOTATION
 182 Notation RX := (cpoly_cring R).
 183 *)
 184
 185 (* end hide *)
 186
 187 inline procedural "cic:/CoRN/algebra/CPoly_ApZero/Cpoly_apzero_interval.con".
 188
 189 (* UNEXPORTED
 190 End Poly_ApZero_Interval
 191 *)
 192