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".
19 (* $Id: OddPolyRootIR.v,v 1.5 2004/04/23 10:01:05 lcf Exp $ *)
25 (*#* * Roots of polynomials of odd degree *)
31 (*#* ** Monic polynomials are positive near infinity
32 %\begin{convention}% Let [R] be an ordered field.
36 inline cic:/CoRN/reals/OddPolyRootIR/R.var.
40 inline cic:/CoRN/reals/OddPolyRootIR/RX.con.
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 inline cic:/CoRN/reals/OddPolyRootIR/R.var.
69 inline cic:/CoRN/reals/OddPolyRootIR/RX.con.
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.
94 Section OddPoly_Signs.
97 (*#* ** Sign of a polynomial of odd degree
98 %\begin{convention}% Let [R] be an ordered field.
102 inline cic:/CoRN/reals/OddPolyRootIR/R.var.
106 inline cic:/CoRN/reals/OddPolyRootIR/RX.con.
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 inline cic:/CoRN/reals/OddPolyRootIR/R.var.
134 inline cic:/CoRN/reals/OddPolyRootIR/RX.con.
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.
151 Section OddPoly_Root.
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.