Section Field_axioms
*)
-inline "cic:/CoRN/algebra/CFields/Field_axioms/F.var" "Field_axioms__".
+alias id "F" = "cic:/CoRN/algebra/CFields/Field_axioms/F.var".
inline "cic:/CoRN/algebra/CFields/CField_is_CField.con".
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CFields/Field_basics/F.var" "Field_basics__".
+alias id "F" = "cic:/CoRN/algebra/CFields/Field_basics/F.var".
inline "cic:/CoRN/algebra/CFields/rcpcl_is_inverse_unfolded.con".
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CFields/Field_multiplication/F.var" "Field_multiplication__".
+alias id "F" = "cic:/CoRN/algebra/CFields/Field_multiplication/F.var".
inline "cic:/CoRN/algebra/CFields/mult_resp_ap_zero.con".
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CFields/Rcpcl_properties/F.var" "Rcpcl_properties__".
+alias id "F" = "cic:/CoRN/algebra/CFields/Rcpcl_properties/F.var".
inline "cic:/CoRN/algebra/CFields/inv_one.con".
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CFields/MultipGroup/F.var" "MultipGroup__".
+alias id "F" = "cic:/CoRN/algebra/CFields/MultipGroup/F.var".
(*#*
The multiplicative monoid of NonZeros.
%\end{nameconvention}%
*)
-inline "cic:/CoRN/algebra/CFields/Div_properties/F.var" "Div_properties__".
+alias id "F" = "cic:/CoRN/algebra/CFields/Div_properties/F.var".
inline "cic:/CoRN/algebra/CFields/div_prop.con".
Section Mult_Cancel_Ap_Zero
*)
-inline "cic:/CoRN/algebra/CFields/Mult_Cancel_Ap_Zero/F.var" "Mult_Cancel_Ap_Zero__".
+alias id "F" = "cic:/CoRN/algebra/CFields/Mult_Cancel_Ap_Zero/F.var".
inline "cic:/CoRN/algebra/CFields/mult_cancel_ap_zero_lft.con".
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CFields/CField_Ops/X.var" "CField_Ops__".
+alias id "X" = "cic:/CoRN/algebra/CFields/CField_Ops/X.var".
-inline "cic:/CoRN/algebra/CFields/CField_Ops/F.var" "CField_Ops__".
+alias id "F" = "cic:/CoRN/algebra/CFields/CField_Ops/F.var".
-inline "cic:/CoRN/algebra/CFields/CField_Ops/G.var" "CField_Ops__".
+alias id "G" = "cic:/CoRN/algebra/CFields/CField_Ops/G.var".
(* begin hide *)
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CFields/CField_Ops/R.var" "CField_Ops__".
+alias id "R" = "cic:/CoRN/algebra/CFields/CField_Ops/R.var".
inline "cic:/CoRN/algebra/CFields/included_FRecip.con".