set "baseuri" "cic:/matita/CoRN-Decl/algebra/CPoly_Degree".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: CPoly_Degree.v,v 1.5 2004/04/23 10:00:53 lcf Exp $ *)
*)
(* UNEXPORTED
-Section Degree_def.
+Section Degree_def
*)
-inline "cic:/CoRN/algebra/CPoly_Degree/R.var".
+alias id "R" = "cic:/CoRN/algebra/CPoly_Degree/Degree_def/R.var".
(* begin hide *)
+(* NOTATION
+Notation RX := (cpoly_cring R).
+*)
+
(* end hide *)
(*#*
inline "cic:/CoRN/algebra/CPoly_Degree/regular.con".
(* UNEXPORTED
-End Degree_def.
+End Degree_def
*)
(* UNEXPORTED
*)
(* UNEXPORTED
-Section Degree_props.
+Section Degree_props
*)
-inline "cic:/CoRN/algebra/CPoly_Degree/R.var".
+alias id "R" = "cic:/CoRN/algebra/CPoly_Degree/Degree_props/R.var".
(* begin hide *)
+(* NOTATION
+Notation RX := (cpoly_cring R).
+*)
+
(* end hide *)
inline "cic:/CoRN/algebra/CPoly_Degree/degree_le_wd.con".
inline "cic:/CoRN/algebra/CPoly_Degree/monic_apzero.con".
(* UNEXPORTED
-End Degree_props.
+End Degree_props
*)
(* UNEXPORTED
*)
(* UNEXPORTED
-Section degree_props_Field.
+Section degree_props_Field
*)
(*#* ** Degrees of polynomials over a field
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CPoly_Degree/F.var".
+alias id "F" = "cic:/CoRN/algebra/CPoly_Degree/degree_props_Field/F.var".
(* begin hide *)
+(* NOTATION
+Notation FX := (cpoly_cring F).
+*)
+
(* end hide *)
inline "cic:/CoRN/algebra/CPoly_Degree/degree_mult.con".
inline "cic:/CoRN/algebra/CPoly_Degree/degree_mult_imp.con".
(* UNEXPORTED
-End degree_props_Field.
+End degree_props_Field
*)