*)
(* UNEXPORTED
-Section CC_ap_zero.
+Section CC_ap_zero
*)
inline "cic:/CoRN/complex/NRootCC/cc_ap_zero.con".
inline "cic:/CoRN/complex/NRootCC/C_cc_ap_zero.con".
(* UNEXPORTED
-End CC_ap_zero.
+End CC_ap_zero
*)
(*#* Weird lemma. *)
(* UNEXPORTED
-Section Imag_to_Real.
+Section Imag_to_Real
*)
inline "cic:/CoRN/complex/NRootCC/imag_to_real.con".
(* UNEXPORTED
-End Imag_to_Real.
+End Imag_to_Real
*)
(*#* ** Roots of the imaginary unit *)
(* UNEXPORTED
-Section NRootI.
+Section NRootI
*)
inline "cic:/CoRN/complex/NRootCC/sqrt_Half.con".
inline "cic:/CoRN/complex/NRootCC/nroot_minus_I_nexp.con".
(* UNEXPORTED
-End NRootI.
+End NRootI
*)
(*#* ** Roots of complex numbers *)
(* UNEXPORTED
-Section NRootCC_1.
+Section NRootCC_1
*)
(*#* We define the nth root of a complex number with a non zero imaginary part.
*)
(* UNEXPORTED
-Section NRootCC_1_ap_real.
+Section NRootCC_1_ap_real
*)
(*#*
%\end{convention}%
*)
-inline "cic:/CoRN/complex/NRootCC/a.var".
+alias id "a" = "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/a.var".
-inline "cic:/CoRN/complex/NRootCC/b.var".
+alias id "b" = "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/b.var".
-inline "cic:/CoRN/complex/NRootCC/b_.var".
+alias id "b_" = "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/b_.var".
(* begin hide *)
-inline "cic:/CoRN/complex/NRootCC/c2.con".
+inline "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/c2.con" "NRootCC_1__NRootCC_1_ap_real__".
(* end hide *)
(* begin hide *)
-inline "cic:/CoRN/complex/NRootCC/c.con".
+inline "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/c.con" "NRootCC_1__NRootCC_1_ap_real__".
-inline "cic:/CoRN/complex/NRootCC/a'2.con".
+inline "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/a'2.con" "NRootCC_1__NRootCC_1_ap_real__".
(* end hide *)
(* begin hide *)
-inline "cic:/CoRN/complex/NRootCC/a'.con".
+inline "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/a'.con" "NRootCC_1__NRootCC_1_ap_real__".
-inline "cic:/CoRN/complex/NRootCC/b'2.con".
+inline "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/b'2.con" "NRootCC_1__NRootCC_1_ap_real__".
(* end hide *)
(* begin hide *)
-inline "cic:/CoRN/complex/NRootCC/b'.con".
+inline "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_real/b'.con" "NRootCC_1__NRootCC_1_ap_real__".
(* end hide *)
inline "cic:/CoRN/complex/NRootCC/nrootCC_1_ap_real.con".
(* UNEXPORTED
-End NRootCC_1_ap_real.
+End NRootCC_1_ap_real
*)
(*#* We now define the nth root of a complex number with a non zero real part.
*)
(* UNEXPORTED
-Section NRootCC_1_ap_imag.
+Section NRootCC_1_ap_imag
*)
(*#*
%\end{convention}%
*)
-inline "cic:/CoRN/complex/NRootCC/a.var".
+alias id "a" = "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_imag/a.var".
-inline "cic:/CoRN/complex/NRootCC/b.var".
+alias id "b" = "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_imag/b.var".
-inline "cic:/CoRN/complex/NRootCC/a_.var".
+alias id "a_" = "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_imag/a_.var".
(* begin hide *)
-inline "cic:/CoRN/complex/NRootCC/c'.con".
+inline "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_imag/c'.con" "NRootCC_1__NRootCC_1_ap_imag__".
-inline "cic:/CoRN/complex/NRootCC/a'.con".
+inline "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_imag/a'.con" "NRootCC_1__NRootCC_1_ap_imag__".
-inline "cic:/CoRN/complex/NRootCC/b'.con".
+inline "cic:/CoRN/complex/NRootCC/NRootCC_1/NRootCC_1_ap_imag/b'.con" "NRootCC_1__NRootCC_1_ap_imag__".
(* end hide *)
inline "cic:/CoRN/complex/NRootCC/nrootCC_1_ap_imag.con".
(* UNEXPORTED
-End NRootCC_1_ap_imag.
+End NRootCC_1_ap_imag
*)
(*#* We now define the roots of arbitrary non zero complex numbers. *)
inline "cic:/CoRN/complex/NRootCC/nrootCC_1.con".
(* UNEXPORTED
-End NRootCC_1.
+End NRootCC_1
*)
(* UNEXPORTED
-Section NRootCC_2.
+Section NRootCC_2
*)
(*#*
%\end{convention}%
*)
-inline "cic:/CoRN/complex/NRootCC/n.var".
+alias id "n" = "cic:/CoRN/complex/NRootCC/NRootCC_2/n.var".
-inline "cic:/CoRN/complex/NRootCC/c.var".
+alias id "c" = "cic:/CoRN/complex/NRootCC/NRootCC_2/c.var".
-inline "cic:/CoRN/complex/NRootCC/z.var".
+alias id "z" = "cic:/CoRN/complex/NRootCC/NRootCC_2/z.var".
-inline "cic:/CoRN/complex/NRootCC/c_.var".
+alias id "c_" = "cic:/CoRN/complex/NRootCC/NRootCC_2/c_.var".
inline "cic:/CoRN/complex/NRootCC/nrootCC_2'.con".
inline "cic:/CoRN/complex/NRootCC/nrootCC_2.con".
(* UNEXPORTED
-End NRootCC_2.
+End NRootCC_2
*)
(* UNEXPORTED
-Section NRootCC_3.
+Section NRootCC_3
*)
inline "cic:/CoRN/complex/NRootCC/Im_poly.con".
%\end{convention}%
*)
-inline "cic:/CoRN/complex/NRootCC/a.var".
+alias id "a" = "cic:/CoRN/complex/NRootCC/NRootCC_3/a.var".
-inline "cic:/CoRN/complex/NRootCC/b.var".
+alias id "b" = "cic:/CoRN/complex/NRootCC/NRootCC_3/b.var".
-inline "cic:/CoRN/complex/NRootCC/b_.var".
+alias id "b_" = "cic:/CoRN/complex/NRootCC/NRootCC_3/b_.var".
-inline "cic:/CoRN/complex/NRootCC/n.var".
+alias id "n" = "cic:/CoRN/complex/NRootCC/NRootCC_3/n.var".
inline "cic:/CoRN/complex/NRootCC/nrCC3_poly''.con".
inline "cic:/CoRN/complex/NRootCC/nrootCC_3_degree.con".
(* UNEXPORTED
-End NRootCC_3.
+End NRootCC_3
*)
(* UNEXPORTED
-Section NRootCC_3'.
+Section NRootCC_3'
*)
(*#*
%\end{convention}%
*)
-inline "cic:/CoRN/complex/NRootCC/c.var".
+alias id "c" = "cic:/CoRN/complex/NRootCC/NRootCC_3'/c.var".
-inline "cic:/CoRN/complex/NRootCC/n.var".
+alias id "n" = "cic:/CoRN/complex/NRootCC/NRootCC_3'/n.var".
-inline "cic:/CoRN/complex/NRootCC/n_.var".
+alias id "n_" = "cic:/CoRN/complex/NRootCC/NRootCC_3'/n_.var".
inline "cic:/CoRN/complex/NRootCC/nrootCC_3'_poly.con".
inline "cic:/CoRN/complex/NRootCC/nrootCC_3'_degree.con".
(* UNEXPORTED
-End NRootCC_3'.
+End NRootCC_3'
*)
(* UNEXPORTED
-Section NRootCC_4.
+Section NRootCC_4
*)
(* UNEXPORTED
-Section NRootCC_4_ap_real.
+Section NRootCC_4_ap_real
*)
(*#*
%\end{convention}%
*)
-inline "cic:/CoRN/complex/NRootCC/a.var".
+alias id "a" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/a.var".
-inline "cic:/CoRN/complex/NRootCC/b.var".
+alias id "b" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/b.var".
-inline "cic:/CoRN/complex/NRootCC/b_.var".
+alias id "b_" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/b_.var".
-inline "cic:/CoRN/complex/NRootCC/n.var".
+alias id "n" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/n.var".
-inline "cic:/CoRN/complex/NRootCC/n_.var".
+alias id "n_" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/n_.var".
(* begin hide *)
-inline "cic:/CoRN/complex/NRootCC/c.con".
+inline "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/c.con" "NRootCC_4__NRootCC_4_ap_real__".
(* end hide *)
(* UNEXPORTED
-Section NRootCC_4_solutions.
+Section NRootCC_4_solutions
*)
(* UNEXPORTED
%\end{convention}%
*)
-inline "cic:/CoRN/complex/NRootCC/r2'.var".
+alias id "r2'" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_solutions/r2'.var".
-inline "cic:/CoRN/complex/NRootCC/c2.var".
+alias id "c2" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_solutions/c2.var".
-inline "cic:/CoRN/complex/NRootCC/r2'_.var".
+alias id "r2'_" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_solutions/r2'_.var".
(* UNEXPORTED
Hint Resolve nrootCC_3': algebra.
inline "cic:/CoRN/complex/NRootCC/nrCC4_a1'.con".
(* UNEXPORTED
-End NRootCC_4_solutions.
+End NRootCC_4_solutions
*)
(* UNEXPORTED
-Section NRootCC_4_equations.
+Section NRootCC_4_equations
*)
(*#*
%\end{convention}%
*)
-inline "cic:/CoRN/complex/NRootCC/r.var".
+alias id "r" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_equations/r.var".
-inline "cic:/CoRN/complex/NRootCC/r_property.var".
+alias id "r_property" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_equations/r_property.var".
-inline "cic:/CoRN/complex/NRootCC/y2.var".
+alias id "y2" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_equations/y2.var".
-inline "cic:/CoRN/complex/NRootCC/y2_property.var".
+alias id "y2_property" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_equations/y2_property.var".
inline "cic:/CoRN/complex/NRootCC/nrCC4_a2.con".
inline "cic:/CoRN/complex/NRootCC/nrCC4_y.con".
-inline "cic:/CoRN/complex/NRootCC/y.con".
+inline "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_equations/y.con" "NRootCC_4__NRootCC_4_ap_real__NRootCC_4_equations__".
inline "cic:/CoRN/complex/NRootCC/nrCC4_x.con".
-inline "cic:/CoRN/complex/NRootCC/x.con".
+inline "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_equations/x.con" "NRootCC_4__NRootCC_4_ap_real__NRootCC_4_equations__".
inline "cic:/CoRN/complex/NRootCC/nrCC4_a5.con".
inline "cic:/CoRN/complex/NRootCC/nrCC4_z.con".
-inline "cic:/CoRN/complex/NRootCC/z.con".
+inline "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_real/NRootCC_4_equations/z.con" "NRootCC_4__NRootCC_4_ap_real__NRootCC_4_equations__".
inline "cic:/CoRN/complex/NRootCC/nrCC4_a7.con".
inline "cic:/CoRN/complex/NRootCC/nrCC4_a9.con".
(* UNEXPORTED
-End NRootCC_4_equations.
+End NRootCC_4_equations
*)
inline "cic:/CoRN/complex/NRootCC/nrCC4_a10.con".
inline "cic:/CoRN/complex/NRootCC/nrootCC_4_ap_real.con".
(* UNEXPORTED
-End NRootCC_4_ap_real.
+End NRootCC_4_ap_real
*)
(* UNEXPORTED
-Section NRootCC_4_ap_imag.
+Section NRootCC_4_ap_imag
*)
(*#*
%\end{convention}%
*)
-inline "cic:/CoRN/complex/NRootCC/a.var".
+alias id "a" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/a.var".
-inline "cic:/CoRN/complex/NRootCC/b.var".
+alias id "b" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/b.var".
-inline "cic:/CoRN/complex/NRootCC/a_.var".
+alias id "a_" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/a_.var".
-inline "cic:/CoRN/complex/NRootCC/n.var".
+alias id "n" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/n.var".
-inline "cic:/CoRN/complex/NRootCC/n_.var".
+alias id "n_" = "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/n_.var".
(* begin hide *)
-inline "cic:/CoRN/complex/NRootCC/c'.con".
+inline "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/c'.con" "NRootCC_4__NRootCC_4_ap_imag__".
-inline "cic:/CoRN/complex/NRootCC/a'.con".
+inline "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/a'.con" "NRootCC_4__NRootCC_4_ap_imag__".
-inline "cic:/CoRN/complex/NRootCC/b'.con".
+inline "cic:/CoRN/complex/NRootCC/NRootCC_4/NRootCC_4_ap_imag/b'.con" "NRootCC_4__NRootCC_4_ap_imag__".
(* end hide *)
inline "cic:/CoRN/complex/NRootCC/nrootCC_4_ap_imag.con".
(* UNEXPORTED
-End NRootCC_4_ap_imag.
+End NRootCC_4_ap_imag
*)
inline "cic:/CoRN/complex/NRootCC/nrootCC_4.con".
(* UNEXPORTED
-End NRootCC_4.
+End NRootCC_4
*)
(*#* Finally, the general definition of nth root. *)
(* UNEXPORTED
-Section NRootCC_5.
+Section NRootCC_5
*)
inline "cic:/CoRN/complex/NRootCC/nrCC_5a2.con".
%\end{convention}%
*)
-inline "cic:/CoRN/complex/NRootCC/c.var".
+alias id "c" = "cic:/CoRN/complex/NRootCC/NRootCC_5/c.var".
-inline "cic:/CoRN/complex/NRootCC/c_.var".
+alias id "c_" = "cic:/CoRN/complex/NRootCC/NRootCC_5/c_.var".
inline "cic:/CoRN/complex/NRootCC/nrCC_5a4.con".
inline "cic:/CoRN/complex/NRootCC/nrootCC_5.con".
(* UNEXPORTED
-End NRootCC_5.
+End NRootCC_5
*)
(*#* Final definition *)