]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/procedural/CoRN/fta/CPoly_Rev.mma
partial update in delayed_updating
[helm.git] / matita / matita / contribs / procedural / CoRN / fta / CPoly_Rev.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_Rev.v,v 1.3 2004/04/23 10:00:56 lcf Exp $ *)
20
21 include "algebra/CPoly_Degree.ma".
22
23 (*#* * Reverse of polynomials
24 *)
25
26 (* UNEXPORTED
27 Section Monomials
28 *)
29
30 (*#*
31 %\begin{convention}% Let [R] be a ring, and let [RX] be the
32 polynomials over this ring.
33 %\end{convention}%
34 *)
35
36 (* UNEXPORTED
37 cic:/CoRN/fta/CPoly_Rev/Monomials/R.var
38 *)
39
40 (* begin hide *)
41
42 inline procedural "cic:/CoRN/fta/CPoly_Rev/Monomials/RX.con" "Monomials__" as definition.
43
44 (* end hide *)
45
46 inline procedural "cic:/CoRN/fta/CPoly_Rev/monom.con" as definition.
47
48 inline procedural "cic:/CoRN/fta/CPoly_Rev/monom_coeff.con" as lemma.
49
50 inline procedural "cic:/CoRN/fta/CPoly_Rev/monom_coeff'.con" as lemma.
51
52 (* UNEXPORTED
53 Hint Resolve monom_coeff monom_coeff': algebra.
54 *)
55
56 inline procedural "cic:/CoRN/fta/CPoly_Rev/monom_degree.con" as lemma.
57
58 inline procedural "cic:/CoRN/fta/CPoly_Rev/monom_S.con" as lemma.
59
60 (* UNEXPORTED
61 Hint Resolve monom_S: algebra.
62 *)
63
64 inline procedural "cic:/CoRN/fta/CPoly_Rev/monom_wd_lft.con" as lemma.
65
66 (* UNEXPORTED
67 Hint Resolve monom_wd_lft: algebra_c.
68 *)
69
70 inline procedural "cic:/CoRN/fta/CPoly_Rev/monom_mult'.con" as lemma.
71
72 (* UNEXPORTED
73 Hint Resolve monom_mult': algebra.
74 *)
75
76 inline procedural "cic:/CoRN/fta/CPoly_Rev/monom_mult.con" as lemma.
77
78 inline procedural "cic:/CoRN/fta/CPoly_Rev/monom_sum.con" as lemma.
79
80 (* UNEXPORTED
81 End Monomials
82 *)
83
84 (* UNEXPORTED
85 Hint Resolve monom_coeff monom_coeff' monom_mult monom_sum: algebra.
86 *)
87
88 (* UNEXPORTED
89 Implicit Arguments monom [R].
90 *)
91
92 (* UNEXPORTED
93 Section Poly_Reverse
94 *)
95
96 (* UNEXPORTED
97 cic:/CoRN/fta/CPoly_Rev/Poly_Reverse/R.var
98 *)
99
100 (* begin hide *)
101
102 inline procedural "cic:/CoRN/fta/CPoly_Rev/Poly_Reverse/RX.con" "Poly_Reverse__" as definition.
103
104 (* end hide *)
105
106 inline procedural "cic:/CoRN/fta/CPoly_Rev/Rev.con" as definition.
107
108 inline procedural "cic:/CoRN/fta/CPoly_Rev/Rev_coeff.con" as lemma.
109
110 inline procedural "cic:/CoRN/fta/CPoly_Rev/Rev_coeff'.con" as lemma.
111
112 (* UNEXPORTED
113 Hint Resolve Rev_coeff Rev_coeff': algebra.
114 *)
115
116 inline procedural "cic:/CoRN/fta/CPoly_Rev/Rev_wd.con" as lemma.
117
118 (* UNEXPORTED
119 Hint Resolve Rev_wd: algebra_c.
120 *)
121
122 inline procedural "cic:/CoRN/fta/CPoly_Rev/Rev_rev.con" as lemma.
123
124 (* UNEXPORTED
125 Hint Resolve Rev_rev: algebra.
126 *)
127
128 inline procedural "cic:/CoRN/fta/CPoly_Rev/Rev_degree_le.con" as lemma.
129
130 inline procedural "cic:/CoRN/fta/CPoly_Rev/Rev_degree.con" as lemma.
131
132 inline procedural "cic:/CoRN/fta/CPoly_Rev/Rev_monom.con" as lemma.
133
134 (* UNEXPORTED
135 Hint Resolve Rev_monom: algebra.
136 *)
137
138 inline procedural "cic:/CoRN/fta/CPoly_Rev/Rev_zero.con" as lemma.
139
140 (* UNEXPORTED
141 Hint Resolve Rev_zero: algebra.
142 *)
143
144 inline procedural "cic:/CoRN/fta/CPoly_Rev/Rev_plus.con" as lemma.
145
146 (* UNEXPORTED
147 Hint Resolve Rev_plus: algebra.
148 *)
149
150 inline procedural "cic:/CoRN/fta/CPoly_Rev/Rev_minus.con" as lemma.
151
152 (* UNEXPORTED
153 Hint Resolve Rev_minus: algebra.
154 *)
155
156 inline procedural "cic:/CoRN/fta/CPoly_Rev/Rev_sum0.con" as lemma.
157
158 (* UNEXPORTED
159 Hint Resolve Rev_sum0: algebra.
160 *)
161
162 inline procedural "cic:/CoRN/fta/CPoly_Rev/Rev_sum.con" as lemma.
163
164 inline procedural "cic:/CoRN/fta/CPoly_Rev/Rev_mult.con" as lemma.
165
166 (* UNEXPORTED
167 End Poly_Reverse
168 *)
169
170 (* UNEXPORTED
171 Hint Resolve Rev_wd: algebra_c.
172 *)
173
174 (* UNEXPORTED
175 Hint Resolve Rev_rev Rev_mult: algebra.
176 *)
177
178 (* UNEXPORTED
179 Implicit Arguments Rev [R].
180 *)
181