(*#* * Roots of polynomials of odd degree *)
(* UNEXPORTED
-Section CPoly_Big.
+Section CPoly_Big
*)
(*#* ** Monic polynomials are positive near infinity
%\end{convention}%
*)
-inline "cic:/CoRN/reals/OddPolyRootIR/R.var".
+alias id "R" = "cic:/CoRN/reals/OddPolyRootIR/CPoly_Big/R.var".
(* begin hide *)
-inline "cic:/CoRN/reals/OddPolyRootIR/RX.con".
+inline "cic:/CoRN/reals/OddPolyRootIR/CPoly_Big/RX.con" "CPoly_Big__".
(* end hide *)
inline "cic:/CoRN/reals/OddPolyRootIR/Ccpoly_pos'.con".
(* UNEXPORTED
-End CPoly_Big.
+End CPoly_Big
*)
(* UNEXPORTED
-Section Flip_Poly.
+Section Flip_Poly
*)
(*#* **Flipping a polynomial
%\end{convention}%
*)
-inline "cic:/CoRN/reals/OddPolyRootIR/R.var".
+alias id "R" = "cic:/CoRN/reals/OddPolyRootIR/Flip_Poly/R.var".
(* begin hide *)
-inline "cic:/CoRN/reals/OddPolyRootIR/RX.con".
+inline "cic:/CoRN/reals/OddPolyRootIR/Flip_Poly/RX.con" "Flip_Poly__".
(* end hide *)
inline "cic:/CoRN/reals/OddPolyRootIR/flip_odd.con".
(* UNEXPORTED
-End Flip_Poly.
+End Flip_Poly
*)
(* UNEXPORTED
*)
(* UNEXPORTED
-Section OddPoly_Signs.
+Section OddPoly_Signs
*)
(*#* ** Sign of a polynomial of odd degree
%\end{convention}%
*)
-inline "cic:/CoRN/reals/OddPolyRootIR/R.var".
+alias id "R" = "cic:/CoRN/reals/OddPolyRootIR/OddPoly_Signs/R.var".
(* begin hide *)
-inline "cic:/CoRN/reals/OddPolyRootIR/RX.con".
+inline "cic:/CoRN/reals/OddPolyRootIR/OddPoly_Signs/RX.con" "OddPoly_Signs__".
(* end hide *)
inline "cic:/CoRN/reals/OddPolyRootIR/oddpoly_neg.con".
(* UNEXPORTED
-End OddPoly_Signs.
+End OddPoly_Signs
*)
(* UNEXPORTED
-Section Poly_Norm.
+Section Poly_Norm
*)
(*#* ** The norm of a polynomial
%\end{convention}%
*)
-inline "cic:/CoRN/reals/OddPolyRootIR/R.var".
+alias id "R" = "cic:/CoRN/reals/OddPolyRootIR/Poly_Norm/R.var".
(* begin hide *)
-inline "cic:/CoRN/reals/OddPolyRootIR/RX.con".
+inline "cic:/CoRN/reals/OddPolyRootIR/Poly_Norm/RX.con" "Poly_Norm__".
(* end hide *)
inline "cic:/CoRN/reals/OddPolyRootIR/poly_norm_apply.con".
(* UNEXPORTED
-End Poly_Norm.
+End Poly_Norm
*)
(* UNEXPORTED
-Section OddPoly_Root.
+Section OddPoly_Root
*)
(*#* ** Roots of polynomials of odd degree
inline "cic:/CoRN/reals/OddPolyRootIR/realpolyn_oddhaszero.con".
(* UNEXPORTED
-End OddPoly_Root.
+End OddPoly_Root
*)