X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Falgebra%2FCRings.ma;h=64f84532b806eb0a497a1b84f2e81eef4eb6d09a;hb=5e01cba364607e7937aec2e359c34f049bb0f108;hp=b38bc3109d5632f9fe59aa2626d990a1ff31e9ab;hpb=80110e17ef1d38d71473e9471ce15beddde663bb;p=helm.git diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/CRings.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/CRings.ma index b38bc3109..64f84532b 100644 --- a/helm/software/matita/contribs/CoRN-Decl/algebra/CRings.ma +++ b/helm/software/matita/contribs/CoRN-Decl/algebra/CRings.ma @@ -83,7 +83,7 @@ inline "cic:/CoRN/algebra/CRings/is_CRing.ind". 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". @@ -91,6 +91,10 @@ inline "cic:/CoRN/algebra/CRings/cr_inv.con". inline "cic:/CoRN/algebra/CRings/cr_minus.con". +(* NOTATION +Notation One := (cr_one _). +*) + (* End_SpecReals *) (* Begin_SpecReals *) @@ -106,8 +110,12 @@ and [[*]] with [mult]. Implicit Arguments cr_mult [c]. *) +(* NOTATION +Infix "[*]" := cr_mult (at level 40, left associativity). +*) + (* UNEXPORTED -Section CRing_axioms. +Section CRing_axioms *) (*#* @@ -116,7 +124,7 @@ Section CRing_axioms. %\end{convention}% *) -inline "cic:/CoRN/algebra/CRings/R.var". +inline "cic:/CoRN/algebra/CRings/CRing_axioms/R.var" "CRing_axioms__". inline "cic:/CoRN/algebra/CRings/CRing_is_CRing.con". @@ -141,11 +149,11 @@ inline "cic:/CoRN/algebra/CRings/mult_wdr.con". (* Begin_SpecReals *) (* UNEXPORTED -End CRing_axioms. +End CRing_axioms *) (* UNEXPORTED -Section Ring_constructions. +Section Ring_constructions *) (*#* @@ -155,7 +163,7 @@ Let [R] be a ring. %\end{convention}% *) -inline "cic:/CoRN/algebra/CRings/R.var". +inline "cic:/CoRN/algebra/CRings/Ring_constructions/R.var" "Ring_constructions__". (*#* The multiplicative monoid of a ring is defined as follows. @@ -164,13 +172,13 @@ 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 *) (*#* @@ -179,11 +187,11 @@ Section Ring_unfolded. %\end{convention}% *) -inline "cic:/CoRN/algebra/CRings/R.var". +inline "cic:/CoRN/algebra/CRings/Ring_unfolded/R.var" "Ring_unfolded__". (* begin hide *) -inline "cic:/CoRN/algebra/CRings/mmR.con". +inline "cic:/CoRN/algebra/CRings/Ring_unfolded/mmR.con" "Ring_unfolded__". (* end hide *) @@ -208,7 +216,7 @@ Hint Resolve ring_dist_unfolded: algebra. inline "cic:/CoRN/algebra/CRings/ring_distl_unfolded.con". (* UNEXPORTED -End Ring_unfolded. +End Ring_unfolded *) (* UNEXPORTED @@ -224,7 +232,7 @@ Hint Resolve ring_dist_unfolded ring_distl_unfolded: algebra. *) (* UNEXPORTED -Section Ring_basics. +Section Ring_basics *) (*#* @@ -233,7 +241,7 @@ Section Ring_basics. %\end{convention}% *) -inline "cic:/CoRN/algebra/CRings/R.var". +inline "cic:/CoRN/algebra/CRings/Ring_basics/R.var" "Ring_basics__". inline "cic:/CoRN/algebra/CRings/one_ap_zero.con". @@ -294,7 +302,7 @@ Hint Resolve ring_distl_minus: algebra. *) (* UNEXPORTED -End Ring_basics. +End Ring_basics *) (* UNEXPORTED @@ -326,7 +334,7 @@ especially geared towards CReals. *) (* UNEXPORTED -Section exponentiation. +Section exponentiation *) (*#* @@ -336,7 +344,7 @@ Let [R] be a ring. %\end{convention}% *) -inline "cic:/CoRN/algebra/CRings/R.var". +inline "cic:/CoRN/algebra/CRings/exponentiation/R.var" "exponentiation__". (* End_SpecReals *) @@ -351,11 +359,15 @@ inline "cic:/CoRN/algebra/CRings/nexp_op.con". (* 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]. *) @@ -363,7 +375,7 @@ Implicit Arguments nexp_op [R]. (* Begin_SpecReals *) (* UNEXPORTED -Section nat_injection. +Section nat_injection *) (*#* @@ -372,7 +384,7 @@ Section nat_injection. %\end{convention}% *) -inline "cic:/CoRN/algebra/CRings/R.var". +inline "cic:/CoRN/algebra/CRings/nat_injection/R.var" "nat_injection__". (*#* The injection of Coq natural numbers into a ring is called [nring]. @@ -393,7 +405,7 @@ inline "cic:/CoRN/algebra/CRings/nring_comm_mult.con". (* Begin_SpecReals *) (* UNEXPORTED -End nat_injection. +End nat_injection *) (* End_SpecReals *) @@ -410,6 +422,50 @@ Implicit Arguments nring [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". @@ -425,7 +481,7 @@ In a ring of characteristic zero, [nring] is really an injection. inline "cic:/CoRN/algebra/CRings/nring_different.con". (* UNEXPORTED -Section int_injection. +Section int_injection *) (*#* @@ -435,7 +491,7 @@ Let [R] be a ring. %\end{convention}% *) -inline "cic:/CoRN/algebra/CRings/R.var". +inline "cic:/CoRN/algebra/CRings/int_injection/R.var" "int_injection__". (*#* The injection of Coq integers into a ring is called [zring]. Again, @@ -565,7 +621,7 @@ inline "cic:/CoRN/algebra/CRings/zring_one.con". inline "cic:/CoRN/algebra/CRings/zring_inv_one.con". (* UNEXPORTED -End int_injection. +End int_injection *) (* UNEXPORTED @@ -579,7 +635,7 @@ Hint Resolve pring_convert zring_zero zring_diff zring_plus_nat zring_inv_nat *) (* UNEXPORTED -Section Ring_sums. +Section Ring_sums *) (*#* @@ -588,14 +644,14 @@ Section Ring_sums. %\end{convention}% *) -inline "cic:/CoRN/algebra/CRings/R.var". +inline "cic:/CoRN/algebra/CRings/Ring_sums/R.var" "Ring_sums__". (*#* *** Infinite Ring sums *) (* UNEXPORTED -Section infinite_ring_sums. +Section infinite_ring_sums *) inline "cic:/CoRN/algebra/CRings/Sum_upto.con". @@ -614,11 +670,11 @@ inline "cic:/CoRN/algebra/CRings/seq_from.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 @@ -633,11 +689,11 @@ inline "cic:/CoRN/algebra/CRings/list_sum_upto_O.con". 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 *) (*#* @@ -648,10 +704,10 @@ Let [R] be a ring. *) (* UNEXPORTED -Section Dist_properties. +Section Dist_properties *) -inline "cic:/CoRN/algebra/CRings/R.var". +inline "cic:/CoRN/algebra/CRings/Dist_properties/R.var" "Dist_properties__". inline "cic:/CoRN/algebra/CRings/dist_1b.con". @@ -688,7 +744,7 @@ inline "cic:/CoRN/algebra/CRings/mult_distr_sum_rht.con". inline "cic:/CoRN/algebra/CRings/sumx_const.con". (* UNEXPORTED -End Dist_properties. +End Dist_properties *) (* UNEXPORTED @@ -704,10 +760,10 @@ Let [R] be a ring. *) (* UNEXPORTED -Section NExp_properties. +Section NExp_properties *) -inline "cic:/CoRN/algebra/CRings/R.var". +inline "cic:/CoRN/algebra/CRings/NExp_properties/R.var" "NExp_properties__". inline "cic:/CoRN/algebra/CRings/nexp_wd.con". @@ -808,7 +864,7 @@ Hint Resolve nexp_funny': algebra. *) (* UNEXPORTED -End NExp_properties. +End NExp_properties *) (* UNEXPORTED @@ -819,7 +875,7 @@ Hint Resolve nexp_wd nexp_Sn nexp_plus one_nexp mult_nexp nexp_mult zero_nexp *) (* UNEXPORTED -Section CRing_Ops. +Section CRing_Ops *) (*#* @@ -833,22 +889,22 @@ respectively [P] and [Q]. %\end{convention}% *) -inline "cic:/CoRN/algebra/CRings/R.var". +inline "cic:/CoRN/algebra/CRings/CRing_Ops/R.var" "CRing_Ops__". -inline "cic:/CoRN/algebra/CRings/F.var". +inline "cic:/CoRN/algebra/CRings/CRing_Ops/F.var" "CRing_Ops__". -inline "cic:/CoRN/algebra/CRings/G.var". +inline "cic:/CoRN/algebra/CRings/CRing_Ops/G.var" "CRing_Ops__". (* 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". @@ -856,21 +912,21 @@ 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". +inline "cic:/CoRN/algebra/CRings/CRing_Ops/Part_Function_Nth_Power/n.var" "CRing_Ops__Part_Function_Nth_Power__". 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 *) (*#* @@ -878,7 +934,7 @@ End Part_Function_Nth_Power. %\end{convention}% *) -inline "cic:/CoRN/algebra/CRings/R'.var". +inline "cic:/CoRN/algebra/CRings/CRing_Ops/R'.var" "CRing_Ops__". inline "cic:/CoRN/algebra/CRings/included_FMult.con". @@ -886,14 +942,14 @@ inline "cic:/CoRN/algebra/CRings/included_FMult'.con". inline "cic:/CoRN/algebra/CRings/included_FMult''.con". -inline "cic:/CoRN/algebra/CRings/n.var". +inline "cic:/CoRN/algebra/CRings/CRing_Ops/n.var" "CRing_Ops__". 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". @@ -902,36 +958,48 @@ 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". +inline "cic:/CoRN/algebra/CRings/ScalarMultiplication/R.var" "ScalarMultiplication__". -inline "cic:/CoRN/algebra/CRings/F.var". +inline "cic:/CoRN/algebra/CRings/ScalarMultiplication/F.var" "ScalarMultiplication__". (* 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". +inline "cic:/CoRN/algebra/CRings/ScalarMultiplication/R'.var" "ScalarMultiplication__". inline "cic:/CoRN/algebra/CRings/included_FScalMult.con". inline "cic:/CoRN/algebra/CRings/included_FScalMult'.con". (* UNEXPORTED -End ScalarMultiplication. +End ScalarMultiplication *) (* UNEXPORTED