1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/reals/OddPolyRootIR".
21 (* $Id: OddPolyRootIR.v,v 1.5 2004/04/23 10:01:05 lcf Exp $ *)
23 include "reals/IVT.ma".
25 (*#* * Roots of polynomials of odd degree *)
31 (*#* ** Monic polynomials are positive near infinity
32 %\begin{convention}% Let [R] be an ordered field.
36 alias id "R" = "cic:/CoRN/reals/OddPolyRootIR/CPoly_Big/R.var".
40 inline "cic:/CoRN/reals/OddPolyRootIR/CPoly_Big/RX.con" "CPoly_Big__".
44 inline "cic:/CoRN/reals/OddPolyRootIR/Cbigger.con".
46 inline "cic:/CoRN/reals/OddPolyRootIR/Ccpoly_big.con".
48 inline "cic:/CoRN/reals/OddPolyRootIR/cpoly_pos.con".
50 inline "cic:/CoRN/reals/OddPolyRootIR/Ccpoly_pos'.con".
60 (*#* **Flipping a polynomial
61 %\begin{convention}% Let [R] be a ring.
65 alias id "R" = "cic:/CoRN/reals/OddPolyRootIR/Flip_Poly/R.var".
69 inline "cic:/CoRN/reals/OddPolyRootIR/Flip_Poly/RX.con" "Flip_Poly__".
73 inline "cic:/CoRN/reals/OddPolyRootIR/flip.con".
75 inline "cic:/CoRN/reals/OddPolyRootIR/flip_poly.con".
77 inline "cic:/CoRN/reals/OddPolyRootIR/flip_coefficient.con".
80 Hint Resolve flip_coefficient: algebra.
83 inline "cic:/CoRN/reals/OddPolyRootIR/flip_odd.con".
90 Hint Resolve flip_poly: algebra.
97 (*#* ** Sign of a polynomial of odd degree
98 %\begin{convention}% Let [R] be an ordered field.
102 alias id "R" = "cic:/CoRN/reals/OddPolyRootIR/OddPoly_Signs/R.var".
106 inline "cic:/CoRN/reals/OddPolyRootIR/OddPoly_Signs/RX.con" "OddPoly_Signs__".
110 inline "cic:/CoRN/reals/OddPolyRootIR/oddpoly_pos.con".
112 inline "cic:/CoRN/reals/OddPolyRootIR/oddpoly_pos'.con".
114 inline "cic:/CoRN/reals/OddPolyRootIR/oddpoly_neg.con".
124 (*#* ** The norm of a polynomial
125 %\begin{convention}% Let [R] be a field, and [RX] the polynomials over
130 alias id "R" = "cic:/CoRN/reals/OddPolyRootIR/Poly_Norm/R.var".
134 inline "cic:/CoRN/reals/OddPolyRootIR/Poly_Norm/RX.con" "Poly_Norm__".
138 inline "cic:/CoRN/reals/OddPolyRootIR/poly_norm_aux.con".
140 inline "cic:/CoRN/reals/OddPolyRootIR/poly_norm.con".
142 inline "cic:/CoRN/reals/OddPolyRootIR/poly_norm_monic.con".
144 inline "cic:/CoRN/reals/OddPolyRootIR/poly_norm_apply.con".
154 (*#* ** Roots of polynomials of odd degree
155 Polynomials of odd degree over the reals always have a root. *)
157 inline "cic:/CoRN/reals/OddPolyRootIR/oddpoly_root'.con".
159 inline "cic:/CoRN/reals/OddPolyRootIR/oddpoly_root.con".
161 inline "cic:/CoRN/reals/OddPolyRootIR/realpolyn_oddhaszero.con".