]> matita.cs.unibo.it Git - helm.git/blob - helm/software/matita/contribs/procedural/CoRN/algebra/CPoly_Degree.mma
transcript: we improved the parser/lexer to read the scripts of the standard
[helm.git] / helm / software / matita / contribs / procedural / CoRN / algebra / CPoly_Degree.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_Degree.v,v 1.5 2004/04/23 10:00:53 lcf Exp $ *)
20
21 include "algebra/CPoly_NthCoeff.ma".
22
23 include "algebra/CFields.ma".
24
25 (*#* *Degrees of Polynomials
26 ** Degrees of polynomials over a ring
27 %\begin{convention}%
28 Let [R] be a ring and write [RX] for the ring of polynomials
29 over [R].
30 %\end{convention}%
31 *)
32
33 (* UNEXPORTED
34 Section Degree_def
35 *)
36
37 (* UNEXPORTED
38 cic:/CoRN/algebra/CPoly_Degree/Degree_def/R.var
39 *)
40
41 (* begin hide *)
42
43 (* NOTATION
44 Notation RX := (cpoly_cring R).
45 *)
46
47 (* end hide *)
48
49 (*#*
50 The length of a polynomial is the number of its coefficients. This is
51 a syntactical property, as the highest coefficient may be [0]. Note that
52 the `zero' polynomial [cpoly_zero] has length [0],
53 a constant polynomial has length [1] and so forth. So the length
54 is always [1] higher than the `degree' (assuming that the highest
55 coefficient is [[#]Zero])!
56 *)
57
58 inline procedural "cic:/CoRN/algebra/CPoly_Degree/lth_of_poly.con" as definition.
59
60 (*#*
61 When dealing with constructive polynomials, notably over the reals or
62 complex numbers, the degree may be unknown, as we can not decide
63 whether the highest coefficient is [[#]Zero]. Hence,
64 degree is a relation between polynomials and natural numbers; if the
65 degree is unknown for polynomial [p], degree(n,p) doesn't hold for
66 any [n].  If we don't know the degree of [p], we may still
67 know it to be below or above a certain number. E.g. for the polynomial
68 $p_0 +p_1 X +\cdots + p_{n-1} X^{n-1}$#p0 +p1 X + ... + p(n-1)
69 X^(n-1)#, if $p_i \mathrel{\#}0$#pi apart from 0#, we can say that the
70 `degree is at least [i]' and if $p_{j+1} = \ldots =p_n =0$#p(j+1)
71 = ... =pn =0# (with [n] the length of the polynomial), we can say
72 that the `degree is at most [j]'.
73 *)
74
75 inline procedural "cic:/CoRN/algebra/CPoly_Degree/degree_le.con" as definition.
76
77 inline procedural "cic:/CoRN/algebra/CPoly_Degree/degree.con" as definition.
78
79 inline procedural "cic:/CoRN/algebra/CPoly_Degree/monic.con" as definition.
80
81 inline procedural "cic:/CoRN/algebra/CPoly_Degree/odd_cpoly.con" as definition.
82
83 inline procedural "cic:/CoRN/algebra/CPoly_Degree/even_cpoly.con" as definition.
84
85 inline procedural "cic:/CoRN/algebra/CPoly_Degree/regular.con" as definition.
86
87 (* UNEXPORTED
88 End Degree_def
89 *)
90
91 (* UNEXPORTED
92 Implicit Arguments degree_le [R].
93 *)
94
95 (* UNEXPORTED
96 Implicit Arguments degree [R].
97 *)
98
99 (* UNEXPORTED
100 Implicit Arguments monic [R].
101 *)
102
103 (* UNEXPORTED
104 Implicit Arguments lth_of_poly [R].
105 *)
106
107 (* UNEXPORTED
108 Section Degree_props
109 *)
110
111 (* UNEXPORTED
112 cic:/CoRN/algebra/CPoly_Degree/Degree_props/R.var
113 *)
114
115 (* begin hide *)
116
117 (* NOTATION
118 Notation RX := (cpoly_cring R).
119 *)
120
121 (* end hide *)
122
123 inline procedural "cic:/CoRN/algebra/CPoly_Degree/degree_le_wd.con" as lemma.
124
125 inline procedural "cic:/CoRN/algebra/CPoly_Degree/degree_wd.con" as lemma.
126
127 inline procedural "cic:/CoRN/algebra/CPoly_Degree/monic_wd.con" as lemma.
128
129 inline procedural "cic:/CoRN/algebra/CPoly_Degree/degree_imp_degree_le.con" as lemma.
130
131 inline procedural "cic:/CoRN/algebra/CPoly_Degree/degree_le_c_.con" as lemma.
132
133 inline procedural "cic:/CoRN/algebra/CPoly_Degree/degree_c_.con" as lemma.
134
135 inline procedural "cic:/CoRN/algebra/CPoly_Degree/monic_c_one.con" as lemma.
136
137 inline procedural "cic:/CoRN/algebra/CPoly_Degree/degree_le_x_.con" as lemma.
138
139 inline procedural "cic:/CoRN/algebra/CPoly_Degree/degree_x_.con" as lemma.
140
141 inline procedural "cic:/CoRN/algebra/CPoly_Degree/monic_x_.con" as lemma.
142
143 inline procedural "cic:/CoRN/algebra/CPoly_Degree/degree_le_mon.con" as lemma.
144
145 inline procedural "cic:/CoRN/algebra/CPoly_Degree/degree_le_inv.con" as lemma.
146
147 inline procedural "cic:/CoRN/algebra/CPoly_Degree/degree_le_plus.con" as lemma.
148
149 inline procedural "cic:/CoRN/algebra/CPoly_Degree/degree_le_minus.con" as lemma.
150
151 inline procedural "cic:/CoRN/algebra/CPoly_Degree/Sum_degree_le.con" as lemma.
152
153 inline procedural "cic:/CoRN/algebra/CPoly_Degree/degree_inv.con" as lemma.
154
155 inline procedural "cic:/CoRN/algebra/CPoly_Degree/degree_plus_rht.con" as lemma.
156
157 inline procedural "cic:/CoRN/algebra/CPoly_Degree/degree_minus_lft.con" as lemma.
158
159 inline procedural "cic:/CoRN/algebra/CPoly_Degree/monic_plus.con" as lemma.
160
161 inline procedural "cic:/CoRN/algebra/CPoly_Degree/monic_minus.con" as lemma.
162
163 inline procedural "cic:/CoRN/algebra/CPoly_Degree/degree_le_mult.con" as lemma.
164
165 inline procedural "cic:/CoRN/algebra/CPoly_Degree/degree_mult_aux.con" as lemma.
166
167 (* UNEXPORTED
168 Hint Resolve degree_mult_aux: algebra.
169 *)
170
171 inline procedural "cic:/CoRN/algebra/CPoly_Degree/monic_mult.con" as lemma.
172
173 inline procedural "cic:/CoRN/algebra/CPoly_Degree/degree_le_nexp.con" as lemma.
174
175 inline procedural "cic:/CoRN/algebra/CPoly_Degree/monic_nexp.con" as lemma.
176
177 inline procedural "cic:/CoRN/algebra/CPoly_Degree/lt_i_lth_of_poly.con" as lemma.
178
179 inline procedural "cic:/CoRN/algebra/CPoly_Degree/poly_degree_lth.con" as lemma.
180
181 inline procedural "cic:/CoRN/algebra/CPoly_Degree/Cpoly_ex_degree.con" as lemma.
182
183 inline procedural "cic:/CoRN/algebra/CPoly_Degree/poly_as_sum''.con" as lemma.
184
185 (* UNEXPORTED
186 Hint Resolve poly_as_sum'': algebra.
187 *)
188
189 inline procedural "cic:/CoRN/algebra/CPoly_Degree/poly_as_sum'.con" as lemma.
190
191 inline procedural "cic:/CoRN/algebra/CPoly_Degree/poly_as_sum.con" as lemma.
192
193 inline procedural "cic:/CoRN/algebra/CPoly_Degree/degree_le_zero.con" as lemma.
194
195 inline procedural "cic:/CoRN/algebra/CPoly_Degree/degree_le_1_imp.con" as lemma.
196
197 inline procedural "cic:/CoRN/algebra/CPoly_Degree/degree_le_cpoly_linear.con" as lemma.
198
199 inline procedural "cic:/CoRN/algebra/CPoly_Degree/monic_cpoly_linear.con" as lemma.
200
201 inline procedural "cic:/CoRN/algebra/CPoly_Degree/monic_one.con" as lemma.
202
203 inline procedural "cic:/CoRN/algebra/CPoly_Degree/monic_apzero.con" as lemma.
204
205 (* UNEXPORTED
206 End Degree_props
207 *)
208
209 (* UNEXPORTED
210 Hint Resolve poly_as_sum'' poly_as_sum' poly_as_sum: algebra.
211 *)
212
213 (* UNEXPORTED
214 Hint Resolve degree_mult_aux: algebra.
215 *)
216
217 (* UNEXPORTED
218 Section degree_props_Field
219 *)
220
221 (*#* ** Degrees of polynomials over a field
222 %\begin{convention}% Let [F] be a field and write [FX] for the ring of
223 polynomials over [F].
224 %\end{convention}%
225 *)
226
227 (* UNEXPORTED
228 cic:/CoRN/algebra/CPoly_Degree/degree_props_Field/F.var
229 *)
230
231 (* begin hide *)
232
233 (* NOTATION
234 Notation FX := (cpoly_cring F).
235 *)
236
237 (* end hide *)
238
239 inline procedural "cic:/CoRN/algebra/CPoly_Degree/degree_mult.con" as lemma.
240
241 inline procedural "cic:/CoRN/algebra/CPoly_Degree/degree_nexp.con" as lemma.
242
243 inline procedural "cic:/CoRN/algebra/CPoly_Degree/degree_le_mult_imp.con" as lemma.
244
245 inline procedural "cic:/CoRN/algebra/CPoly_Degree/degree_mult_imp.con" as lemma.
246
247 (* UNEXPORTED
248 End degree_props_Field
249 *)
250