*)
(* UNEXPORTED
-Section Field_axioms.
+Section Field_axioms
*)
-inline "cic:/CoRN/algebra/CFields/F.var".
+alias id "F" = "cic:/CoRN/algebra/CFields/Field_axioms/F.var".
inline "cic:/CoRN/algebra/CFields/CField_is_CField.con".
inline "cic:/CoRN/algebra/CFields/rcpcl_is_inverse.con".
(* UNEXPORTED
-End Field_axioms.
+End Field_axioms
*)
(* UNEXPORTED
-Section Field_basics.
+Section Field_basics
*)
(*#* ** Field basics
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CFields/F.var".
+alias id "F" = "cic:/CoRN/algebra/CFields/Field_basics/F.var".
inline "cic:/CoRN/algebra/CFields/rcpcl_is_inverse_unfolded.con".
inline "cic:/CoRN/algebra/CFields/field_mult_inv_op.con".
(* UNEXPORTED
-End Field_basics.
+End Field_basics
*)
(* UNEXPORTED
*)
(* UNEXPORTED
-Section Field_multiplication.
+Section Field_multiplication
*)
(*#*
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CFields/F.var".
+alias id "F" = "cic:/CoRN/algebra/CFields/Field_multiplication/F.var".
inline "cic:/CoRN/algebra/CFields/mult_resp_ap_zero.con".
inline "cic:/CoRN/algebra/CFields/cond_square_eq.con".
(* UNEXPORTED
-End Field_multiplication.
+End Field_multiplication
*)
(* UNEXPORTED
-Section x_square.
+Section x_square
*)
inline "cic:/CoRN/algebra/CFields/x_xminone.con".
inline "cic:/CoRN/algebra/CFields/square_id.con".
(* UNEXPORTED
-End x_square.
+End x_square
*)
(* UNEXPORTED
*)
(* UNEXPORTED
-Section Rcpcl_properties.
+Section Rcpcl_properties
*)
(*#*
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CFields/F.var".
+alias id "F" = "cic:/CoRN/algebra/CFields/Rcpcl_properties/F.var".
inline "cic:/CoRN/algebra/CFields/inv_one.con".
inline "cic:/CoRN/algebra/CFields/f_rcpcl_f_rcpcl.con".
(* UNEXPORTED
-End Rcpcl_properties.
+End Rcpcl_properties
*)
(* UNEXPORTED
-Section MultipGroup.
+Section MultipGroup
*)
(*#*
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CFields/F.var".
+alias id "F" = "cic:/CoRN/algebra/CFields/MultipGroup/F.var".
(*#*
The multiplicative monoid of NonZeros.
inline "cic:/CoRN/algebra/CFields/cfield_to_mult_cgroup.con".
(* UNEXPORTED
-End MultipGroup.
+End MultipGroup
*)
(* UNEXPORTED
-Section Div_properties.
+Section Div_properties
*)
(*#*
%\end{nameconvention}%
*)
-inline "cic:/CoRN/algebra/CFields/F.var".
+alias id "F" = "cic:/CoRN/algebra/CFields/Div_properties/F.var".
inline "cic:/CoRN/algebra/CFields/div_prop.con".
inline "cic:/CoRN/algebra/CFields/div_strext.con".
(* UNEXPORTED
-End Div_properties.
+End Div_properties
*)
(* UNEXPORTED
*)
(* UNEXPORTED
-Section Mult_Cancel_Ap_Zero.
+Section Mult_Cancel_Ap_Zero
*)
-inline "cic:/CoRN/algebra/CFields/F.var".
+alias id "F" = "cic:/CoRN/algebra/CFields/Mult_Cancel_Ap_Zero/F.var".
inline "cic:/CoRN/algebra/CFields/mult_cancel_ap_zero_lft.con".
inline "cic:/CoRN/algebra/CFields/recip_resp_ap.con".
(* UNEXPORTED
-End Mult_Cancel_Ap_Zero.
+End Mult_Cancel_Ap_Zero
*)
(* UNEXPORTED
-Section CField_Ops.
+Section CField_Ops
*)
(*#*
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CFields/X.var".
+alias id "X" = "cic:/CoRN/algebra/CFields/CField_Ops/X.var".
-inline "cic:/CoRN/algebra/CFields/F.var".
+alias id "F" = "cic:/CoRN/algebra/CFields/CField_Ops/F.var".
-inline "cic:/CoRN/algebra/CFields/G.var".
+alias id "G" = "cic:/CoRN/algebra/CFields/CField_Ops/G.var".
(* begin hide *)
-inline "cic:/CoRN/algebra/CFields/P.con".
+inline "cic:/CoRN/algebra/CFields/CField_Ops/P.con" "CField_Ops__".
-inline "cic:/CoRN/algebra/CFields/Q.con".
+inline "cic:/CoRN/algebra/CFields/CField_Ops/Q.con" "CField_Ops__".
(* end hide *)
(* UNEXPORTED
-Section Part_Function_Recip.
+Section Part_Function_Recip
*)
(*#*
Some auxiliary notions are helpful in defining the domain.
*)
-inline "cic:/CoRN/algebra/CFields/R.con".
+inline "cic:/CoRN/algebra/CFields/CField_Ops/Part_Function_Recip/R.con" "CField_Ops__Part_Function_Recip__".
-inline "cic:/CoRN/algebra/CFields/Ext2R.con".
+inline "cic:/CoRN/algebra/CFields/CField_Ops/Part_Function_Recip/Ext2R.con" "CField_Ops__Part_Function_Recip__".
inline "cic:/CoRN/algebra/CFields/part_function_recip_strext.con".
inline "cic:/CoRN/algebra/CFields/Frecip.con".
(* UNEXPORTED
-End Part_Function_Recip.
+End Part_Function_Recip
*)
(* UNEXPORTED
-Section Part_Function_Div.
+Section Part_Function_Div
*)
(*#*
For division things work out almost in the same way.
*)
-inline "cic:/CoRN/algebra/CFields/R.con".
+inline "cic:/CoRN/algebra/CFields/CField_Ops/Part_Function_Div/R.con" "CField_Ops__Part_Function_Div__".
-inline "cic:/CoRN/algebra/CFields/Ext2R.con".
+inline "cic:/CoRN/algebra/CFields/CField_Ops/Part_Function_Div/Ext2R.con" "CField_Ops__Part_Function_Div__".
inline "cic:/CoRN/algebra/CFields/part_function_div_strext.con".
inline "cic:/CoRN/algebra/CFields/Fdiv.con".
(* UNEXPORTED
-End Part_Function_Div.
+End Part_Function_Div
*)
(*#*
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CFields/R.var".
+alias id "R" = "cic:/CoRN/algebra/CFields/CField_Ops/R.var".
inline "cic:/CoRN/algebra/CFields/included_FRecip.con".
inline "cic:/CoRN/algebra/CFields/included_FDiv''.con".
(* UNEXPORTED
-End CField_Ops.
+End CField_Ops
*)
(* UNEXPORTED