]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/procedural/CoRN/algebra/CPoly_ApZero.mma
made executable again
[helm.git] / 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