set "baseuri" "cic:/matita/CoRN-Decl/algebra/CRings".
-include "CoRN_notation.ma".
+include "CoRN.ma".
(* $Id: CRings.v,v 1.8 2004/04/23 10:00:53 lcf Exp $ *)
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.
+Section CRing_axioms
*)
(*#*
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CRings/R.var".
+alias id "R" = "cic:/CoRN/algebra/CRings/CRing_axioms/R.var".
inline "cic:/CoRN/algebra/CRings/CRing_is_CRing.con".
(* Begin_SpecReals *)
(* UNEXPORTED
-End CRing_axioms.
+End CRing_axioms
*)
(* UNEXPORTED
-Section Ring_constructions.
+Section Ring_constructions
*)
(*#*
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CRings/R.var".
+alias id "R" = "cic:/CoRN/algebra/CRings/Ring_constructions/R.var".
(*#*
The multiplicative monoid of a ring is defined as follows.
inline "cic:/CoRN/algebra/CRings/Build_multCMonoid.con".
(* UNEXPORTED
-End Ring_constructions.
+End Ring_constructions
*)
(* End_SpecReals *)
(* UNEXPORTED
-Section Ring_unfolded.
+Section Ring_unfolded
*)
(*#*
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CRings/R.var".
+alias id "R" = "cic:/CoRN/algebra/CRings/Ring_unfolded/R.var".
(* begin hide *)
-inline "cic:/CoRN/algebra/CRings/mmR.con".
+inline "cic:/CoRN/algebra/CRings/Ring_unfolded/mmR.con" "Ring_unfolded__".
(* end hide *)
inline "cic:/CoRN/algebra/CRings/ring_distl_unfolded.con".
(* UNEXPORTED
-End Ring_unfolded.
+End Ring_unfolded
*)
(* UNEXPORTED
*)
(* UNEXPORTED
-Section Ring_basics.
+Section Ring_basics
*)
(*#*
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CRings/R.var".
+alias id "R" = "cic:/CoRN/algebra/CRings/Ring_basics/R.var".
inline "cic:/CoRN/algebra/CRings/one_ap_zero.con".
*)
(* UNEXPORTED
-End Ring_basics.
+End Ring_basics
*)
(* UNEXPORTED
*)
(* UNEXPORTED
-Section exponentiation.
+Section exponentiation
*)
(*#*
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CRings/R.var".
+alias id "R" = "cic:/CoRN/algebra/CRings/exponentiation/R.var".
(* End_SpecReals *)
(* Begin_SpecReals *)
(* UNEXPORTED
-End exponentiation.
+End exponentiation
*)
(* End_SpecReals *)
+(* NOTATION
+Notation "x [^] n" := (nexp_op _ n x) (at level 20).
+*)
+
(* UNEXPORTED
Implicit Arguments nexp_op [R].
*)
(* Begin_SpecReals *)
(* UNEXPORTED
-Section nat_injection.
+Section nat_injection
*)
(*#*
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CRings/R.var".
+alias id "R" = "cic:/CoRN/algebra/CRings/nat_injection/R.var".
(*#*
The injection of Coq natural numbers into a ring is called [nring].
(* Begin_SpecReals *)
(* UNEXPORTED
-End nat_injection.
+End nat_injection
*)
(* End_SpecReals *)
(* 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".
inline "cic:/CoRN/algebra/CRings/nring_different.con".
(* UNEXPORTED
-Section int_injection.
+Section int_injection
*)
(*#*
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CRings/R.var".
+alias id "R" = "cic:/CoRN/algebra/CRings/int_injection/R.var".
(*#*
The injection of Coq integers into a ring is called [zring]. Again,
inline "cic:/CoRN/algebra/CRings/zring_inv_one.con".
(* UNEXPORTED
-End int_injection.
+End int_injection
*)
(* UNEXPORTED
*)
(* UNEXPORTED
-Section Ring_sums.
+Section Ring_sums
*)
(*#*
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CRings/R.var".
+alias id "R" = "cic:/CoRN/algebra/CRings/Ring_sums/R.var".
(*#*
*** Infinite Ring sums
*)
(* UNEXPORTED
-Section infinite_ring_sums.
+Section infinite_ring_sums
*)
inline "cic:/CoRN/algebra/CRings/Sum_upto.con".
inline "cic:/CoRN/algebra/CRings/Sum_from_upto_alt.con".
(* UNEXPORTED
-End infinite_ring_sums.
+End infinite_ring_sums
*)
(* UNEXPORTED
-Section ring_sums_over_lists.
+Section ring_sums_over_lists
*)
(*#* *** Ring Sums over Lists
inline "cic:/CoRN/algebra/CRings/List_Sum_from_upto.con".
(* UNEXPORTED
-End ring_sums_over_lists.
+End ring_sums_over_lists
*)
(* UNEXPORTED
-End Ring_sums.
+End Ring_sums
*)
(*#*
*)
(* UNEXPORTED
-Section Dist_properties.
+Section Dist_properties
*)
-inline "cic:/CoRN/algebra/CRings/R.var".
+alias id "R" = "cic:/CoRN/algebra/CRings/Dist_properties/R.var".
inline "cic:/CoRN/algebra/CRings/dist_1b.con".
inline "cic:/CoRN/algebra/CRings/sumx_const.con".
(* UNEXPORTED
-End Dist_properties.
+End Dist_properties
*)
(* UNEXPORTED
*)
(* UNEXPORTED
-Section NExp_properties.
+Section NExp_properties
*)
-inline "cic:/CoRN/algebra/CRings/R.var".
+alias id "R" = "cic:/CoRN/algebra/CRings/NExp_properties/R.var".
inline "cic:/CoRN/algebra/CRings/nexp_wd.con".
*)
(* UNEXPORTED
-End NExp_properties.
+End NExp_properties
*)
(* UNEXPORTED
*)
(* UNEXPORTED
-Section CRing_Ops.
+Section CRing_Ops
*)
(*#*
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CRings/R.var".
+alias id "R" = "cic:/CoRN/algebra/CRings/CRing_Ops/R.var".
-inline "cic:/CoRN/algebra/CRings/F.var".
+alias id "F" = "cic:/CoRN/algebra/CRings/CRing_Ops/F.var".
-inline "cic:/CoRN/algebra/CRings/G.var".
+alias id "G" = "cic:/CoRN/algebra/CRings/CRing_Ops/G.var".
(* begin hide *)
-inline "cic:/CoRN/algebra/CRings/P.con".
+inline "cic:/CoRN/algebra/CRings/CRing_Ops/P.con" "CRing_Ops__".
-inline "cic:/CoRN/algebra/CRings/Q.con".
+inline "cic:/CoRN/algebra/CRings/CRing_Ops/Q.con" "CRing_Ops__".
(* end hide *)
(* UNEXPORTED
-Section Part_Function_Mult.
+Section Part_Function_Mult
*)
inline "cic:/CoRN/algebra/CRings/part_function_mult_strext.con".
inline "cic:/CoRN/algebra/CRings/Fmult.con".
(* UNEXPORTED
-End Part_Function_Mult.
+End Part_Function_Mult
*)
(* UNEXPORTED
-Section Part_Function_Nth_Power.
+Section Part_Function_Nth_Power
*)
-inline "cic:/CoRN/algebra/CRings/n.var".
+alias id "n" = "cic:/CoRN/algebra/CRings/CRing_Ops/Part_Function_Nth_Power/n.var".
inline "cic:/CoRN/algebra/CRings/part_function_nth_strext.con".
inline "cic:/CoRN/algebra/CRings/Fnth.con".
(* UNEXPORTED
-End Part_Function_Nth_Power.
+End Part_Function_Nth_Power
*)
(*#*
%\end{convention}%
*)
-inline "cic:/CoRN/algebra/CRings/R'.var".
+alias id "R'" = "cic:/CoRN/algebra/CRings/CRing_Ops/R'.var".
inline "cic:/CoRN/algebra/CRings/included_FMult.con".
inline "cic:/CoRN/algebra/CRings/included_FMult''.con".
-inline "cic:/CoRN/algebra/CRings/n.var".
+alias id "n" = "cic:/CoRN/algebra/CRings/CRing_Ops/n.var".
inline "cic:/CoRN/algebra/CRings/included_FNth.con".
inline "cic:/CoRN/algebra/CRings/included_FNth'.con".
(* UNEXPORTED
-End CRing_Ops.
+End CRing_Ops
*)
inline "cic:/CoRN/algebra/CRings/Fscalmult.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.
+Section ScalarMultiplication
*)
-inline "cic:/CoRN/algebra/CRings/R.var".
+alias id "R" = "cic:/CoRN/algebra/CRings/ScalarMultiplication/R.var".
-inline "cic:/CoRN/algebra/CRings/F.var".
+alias id "F" = "cic:/CoRN/algebra/CRings/ScalarMultiplication/F.var".
(* begin hide *)
-inline "cic:/CoRN/algebra/CRings/P.con".
+inline "cic:/CoRN/algebra/CRings/ScalarMultiplication/P.con" "ScalarMultiplication__".
(* end hide *)
-inline "cic:/CoRN/algebra/CRings/R'.var".
+alias id "R'" = "cic:/CoRN/algebra/CRings/ScalarMultiplication/R'.var".
inline "cic:/CoRN/algebra/CRings/included_FScalMult.con".
inline "cic:/CoRN/algebra/CRings/included_FScalMult'.con".
(* UNEXPORTED
-End ScalarMultiplication.
+End ScalarMultiplication
*)
(* UNEXPORTED