inline "cic:/CoRN/algebra/CRings/CRing.ind".
-coercion "cic:/matita/CoRN-Decl/algebra/CRings/cr_crr.con" 0 (* compounds *).
+coercion cic:/matita/CoRN-Decl/algebra/CRings/cr_crr.con 0 (* compounds *).
inline "cic:/CoRN/algebra/CRings/cr_plus.con".
inline "cic:/CoRN/algebra/CRings/cr_minus.con".
+(* NOTATION
+Notation One := (cr_one _).
+*)
+
(* End_SpecReals *)
(* Begin_SpecReals *)
Implicit Arguments cr_mult [c].
*)
+(* NOTATION
+Infix "[*]" := cr_mult (at level 40, left associativity).
+*)
+
(* UNEXPORTED
Section CRing_axioms.
*)
(* End_SpecReals *)
+(* NOTATION
+Notation "x [^] n" := (nexp_op _ n x) (at level 20).
+*)
+
(* UNEXPORTED
Implicit Arguments nexp_op [R].
*)
(* End_SpecReals *)
+(* NOTATION
+Notation Two := (nring 2).
+*)
+
+(* NOTATION
+Notation Three := (nring 3).
+*)
+
+(* NOTATION
+Notation Four := (nring 4).
+*)
+
+(* NOTATION
+Notation Six := (nring 6).
+*)
+
+(* NOTATION
+Notation Eight := (nring 8).
+*)
+
+(* NOTATION
+Notation Twelve := (nring 12).
+*)
+
+(* NOTATION
+Notation Sixteen := (nring 16).
+*)
+
+(* NOTATION
+Notation Nine := (nring 9).
+*)
+
+(* NOTATION
+Notation Eighteen := (nring 18).
+*)
+
+(* NOTATION
+Notation TwentyFour := (nring 24).
+*)
+
+(* NOTATION
+Notation FortyEight := (nring 48).
+*)
+
inline "cic:/CoRN/algebra/CRings/one_plus_one.con".
inline "cic:/CoRN/algebra/CRings/x_plus_x.con".
Implicit Arguments Fmult [R].
*)
+(* NOTATION
+Infix "{*}" := Fmult (at level 40, left associativity).
+*)
+
(* UNEXPORTED
Implicit Arguments Fscalmult [R].
*)
+(* NOTATION
+Infix "{**}" := Fscalmult (at level 40, left associativity).
+*)
+
(* UNEXPORTED
Implicit Arguments Fnth [R].
*)
+(* NOTATION
+Infix "{^}" := Fnth (at level 30, right associativity).
+*)
+
(* UNEXPORTED
Section ScalarMultiplication.
*)