X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcontribs%2FCoRN-Decl%2Falgebra%2FCOrdFields.ma;h=cb6476676c55a1c0cbd2aaf1f4d37fe88d19f37b;hb=1776f357e1a69fa1133956660b65d7bafdfe5c25;hp=c68ec867d05355db3b563f6091e37bf469dc1783;hpb=f104e234238586ac846881feb30e1b56a509cfd3;p=helm.git diff --git a/matita/contribs/CoRN-Decl/algebra/COrdFields.ma b/matita/contribs/CoRN-Decl/algebra/COrdFields.ma index c68ec867d..cb6476676 100644 --- a/matita/contribs/CoRN-Decl/algebra/COrdFields.ma +++ b/matita/contribs/CoRN-Decl/algebra/COrdFields.ma @@ -83,7 +83,7 @@ inline "cic:/CoRN/algebra/COrdFields/is_COrdField.ind". inline "cic:/CoRN/algebra/COrdFields/COrdField.ind". -coercion "cic:/matita/CoRN-Decl/algebra/COrdFields/cof_crr.con" 0 (* compounds *). +coercion cic:/matita/CoRN-Decl/algebra/COrdFields/cof_crr.con 0 (* compounds *). (*#* %\begin{nameconvention}% @@ -96,12 +96,20 @@ is written as [pos]. Implicit Arguments cof_less [c]. *) +(* NOTATION +Infix "[<]" := cof_less (at level 70, no associativity). +*) + inline "cic:/CoRN/algebra/COrdFields/greater.con". (* UNEXPORTED Implicit Arguments greater [F]. *) +(* NOTATION +Infix "[>]" := greater (at level 70, no associativity). +*) + (* End_SpecReals *) (*#* @@ -121,8 +129,12 @@ In the names of lemmas, [ [<=] ] is written as [leEq] and Implicit Arguments leEq [F]. *) +(* NOTATION +Infix "[<=]" := leEq (at level 70, no associativity). +*) + (* UNEXPORTED -Section COrdField_axioms. +Section COrdField_axioms *) (*#* @@ -132,7 +144,7 @@ Let [F] be a field. %\end{convention}% *) -inline "cic:/CoRN/algebra/COrdFields/F.var". +alias id "F" = "cic:/CoRN/algebra/COrdFields/COrdField_axioms/F.var". inline "cic:/CoRN/algebra/COrdFields/COrdField_is_COrdField.con". @@ -157,7 +169,7 @@ inline "cic:/CoRN/algebra/COrdFields/less_wdr.con". inline "cic:/CoRN/algebra/COrdFields/less_wdl.con". (* UNEXPORTED -End COrdField_axioms. +End COrdField_axioms *) (* UNEXPORTED @@ -169,7 +181,7 @@ Declare Right Step less_wdr. *) (* UNEXPORTED -Section OrdField_basics. +Section OrdField_basics *) (*#* @@ -183,7 +195,7 @@ Let in the rest of this section (and all subsections) %\end{convention}% *) -inline "cic:/CoRN/algebra/COrdFields/R.var". +alias id "R" = "cic:/CoRN/algebra/COrdFields/OrdField_basics/R.var". inline "cic:/CoRN/algebra/COrdFields/less_imp_ap.con". @@ -206,13 +218,13 @@ inline "cic:/CoRN/algebra/COrdFields/pos_ap_zero.con". inline "cic:/CoRN/algebra/COrdFields/leEq_not_eq.con". (* UNEXPORTED -End OrdField_basics. +End OrdField_basics *) (*#**********************************) (* UNEXPORTED -Section Basic_Properties_of_leEq. +Section Basic_Properties_of_leEq *) (*#**********************************) @@ -220,7 +232,7 @@ Section Basic_Properties_of_leEq. (*#* ** Basic properties of [ [<=] ] *) -inline "cic:/CoRN/algebra/COrdFields/R.var". +alias id "R" = "cic:/CoRN/algebra/COrdFields/Basic_Properties_of_leEq/R.var". inline "cic:/CoRN/algebra/COrdFields/leEq_wdr.con". @@ -251,7 +263,7 @@ inline "cic:/CoRN/algebra/COrdFields/leEq_transitive.con". inline "cic:/CoRN/algebra/COrdFields/less_leEq.con". (* UNEXPORTED -End Basic_Properties_of_leEq. +End Basic_Properties_of_leEq *) (* UNEXPORTED @@ -263,7 +275,7 @@ Declare Right Step leEq_wdr. *) (* UNEXPORTED -Section infinity_of_cordfields. +Section infinity_of_cordfields *) (*#* @@ -276,7 +288,7 @@ and so on. These are elements of [NonZeros], so that we can write e.g.%\% [x[/]TwoNZ]. *) -inline "cic:/CoRN/algebra/COrdFields/R.var". +alias id "R" = "cic:/CoRN/algebra/COrdFields/infinity_of_cordfields/R.var". inline "cic:/CoRN/algebra/COrdFields/pos_one.con". @@ -307,7 +319,7 @@ inline "cic:/CoRN/algebra/COrdFields/nring_fac_ap_zero.con". include "tactics/Opaque_algebra.ma". (* UNEXPORTED -Section up_to_four. +Section up_to_four *) (*#* @@ -349,11 +361,11 @@ inline "cic:/CoRN/algebra/COrdFields/three_ap_zero.con". inline "cic:/CoRN/algebra/COrdFields/four_ap_zero.con". (* UNEXPORTED -End up_to_four. +End up_to_four *) (* UNEXPORTED -Section More_than_four. +Section More_than_four *) (*#* *** Properties of some other numbers *) @@ -391,11 +403,11 @@ inline "cic:/CoRN/algebra/COrdFields/twentyfour_ap_zero.con". inline "cic:/CoRN/algebra/COrdFields/fortyeight_ap_zero.con". (* UNEXPORTED -End More_than_four. +End More_than_four *) (* UNEXPORTED -End infinity_of_cordfields. +End infinity_of_cordfields *) (* UNEXPORTED @@ -406,15 +418,63 @@ Declare Left Step leEq_wdl. Declare Right Step leEq_wdr. *) +(* NOTATION +Notation " x [/]OneNZ" := (x[/] One[//]ring_non_triv _) (at level 20). +*) + +(* NOTATION +Notation " x [/]TwoNZ" := (x[/] Two[//]two_ap_zero _) (at level 20). +*) + +(* NOTATION +Notation " x [/]ThreeNZ" := (x[/] Three[//]three_ap_zero _) (at level 20). +*) + +(* NOTATION +Notation " x [/]FourNZ" := (x[/] Four[//]four_ap_zero _) (at level 20). +*) + +(* NOTATION +Notation " x [/]SixNZ" := (x[/] Six[//]six_ap_zero _) (at level 20). +*) + +(* NOTATION +Notation " x [/]EightNZ" := (x[/] Eight[//]eight_ap_zero _) (at level 20). +*) + +(* NOTATION +Notation " x [/]NineNZ" := (x[/] Nine[//]nine_ap_zero _) (at level 20). +*) + +(* NOTATION +Notation " x [/]TwelveNZ" := (x[/] Twelve[//]twelve_ap_zero _) (at level 20). +*) + +(* NOTATION +Notation " x [/]SixteenNZ" := (x[/] Sixteen[//]sixteen_ap_zero _) (at level 20). +*) + +(* NOTATION +Notation " x [/]EighteenNZ" := (x[/] Eighteen[//]eighteen_ap_zero _) (at level 20). +*) + +(* NOTATION +Notation " x [/]TwentyFourNZ" := (x[/] TwentyFour[//]twentyfour_ap_zero _) (at level 20). +*) + +(* NOTATION +Notation " x [/]FortyEightNZ" := (x[/] FortyEight[//]fortyeight_ap_zero _) (at level 20). +*) + (* UNEXPORTED -Section consequences_of_infinity. +Section consequences_of_infinity *) (*#* *** Consequences of infinity *) -inline "cic:/CoRN/algebra/COrdFields/F.var". +alias id "F" = "cic:/CoRN/algebra/COrdFields/consequences_of_infinity/F.var". inline "cic:/CoRN/algebra/COrdFields/square_eq.con". @@ -425,13 +485,13 @@ Ordered fields have characteristic zero. inline "cic:/CoRN/algebra/COrdFields/char0_OrdField.con". (* UNEXPORTED -End consequences_of_infinity. +End consequences_of_infinity *) (*#**********************************) (* UNEXPORTED -Section Properties_of_Ordering. +Section Properties_of_Ordering *) (*#**********************************) @@ -440,7 +500,7 @@ Section Properties_of_Ordering. ** Properties of [[<]] *) -inline "cic:/CoRN/algebra/COrdFields/R.var". +alias id "R" = "cic:/CoRN/algebra/COrdFields/Properties_of_Ordering/R.var". (*#* We do not use a special predicate for positivity, @@ -451,7 +511,7 @@ Reasons: it is more natural; in ordinary mathematics we also write [Zero [<] x] *) (* UNEXPORTED -Section addition. +Section addition *) (*#* @@ -533,11 +593,11 @@ inline "cic:/CoRN/algebra/COrdFields/shift_zero_less_minus'.con". inline "cic:/CoRN/algebra/COrdFields/qltone.con". (* UNEXPORTED -End addition. +End addition *) (* UNEXPORTED -Section multiplication. +Section multiplication *) (*#* @@ -642,11 +702,11 @@ inline "cic:/CoRN/algebra/COrdFields/pos_div_twentyfour.con". inline "cic:/CoRN/algebra/COrdFields/pos_div_fortyeight.con". (* UNEXPORTED -End multiplication. +End multiplication *) (* UNEXPORTED -Section misc. +Section misc *) (*#* @@ -674,10 +734,10 @@ inline "cic:/CoRN/algebra/COrdFields/positive_Sumx.con". inline "cic:/CoRN/algebra/COrdFields/negative_Sumx.con". (* UNEXPORTED -End misc. +End misc *) (* UNEXPORTED -End Properties_of_Ordering. +End Properties_of_Ordering *)