X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FCoRN-Decl%2Falgebra%2FCFields.ma;h=2daac721ee1a353955e448e2e6818aa9b39b087e;hb=5e01cba364607e7937aec2e359c34f049bb0f108;hp=606136603e6cf7ed4d6a1397754ca99c8546797d;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git

diff --git a/helm/software/matita/contribs/CoRN-Decl/algebra/CFields.ma b/helm/software/matita/contribs/CoRN-Decl/algebra/CFields.ma
index 606136603..2daac721e 100644
--- a/helm/software/matita/contribs/CoRN-Decl/algebra/CFields.ma
+++ b/helm/software/matita/contribs/CoRN-Decl/algebra/CFields.ma
@@ -16,6 +16,8 @@
 
 set "baseuri" "cic:/matita/CoRN-Decl/algebra/CFields".
 
+include "CoRN.ma".
+
 (* $Id: CFields.v,v 1.12 2004/04/23 10:00:52 lcf Exp $ *)
 
 (*#* printing [/] %\ensuremath{/}% #/# *)
@@ -28,9 +30,7 @@ set "baseuri" "cic:/matita/CoRN-Decl/algebra/CFields".
 
 (*#* printing [/]?[//] %\ensuremath{/?\ddagger}% #/?‡# *)
 
-(* INCLUDE
-CRings
-*)
+include "algebra/CRings.ma".
 
 (* UNEXPORTED
 Transparent sym_eq.
@@ -121,15 +121,17 @@ Transparent nexp_op.
 ** Definition of the notion Field
 *)
 
-inline cic:/CoRN/algebra/CFields/is_CField.con.
+inline "cic:/CoRN/algebra/CFields/is_CField.con".
+
+inline "cic:/CoRN/algebra/CFields/CField.ind".
 
-inline cic:/CoRN/algebra/CFields/CField.ind.
+coercion cic:/matita/CoRN-Decl/algebra/CFields/cf_crr.con 0 (* compounds *).
 
 (* End_SpecReals *)
 
-inline cic:/CoRN/algebra/CFields/f_rcpcl'.con.
+inline "cic:/CoRN/algebra/CFields/f_rcpcl'.con".
 
-inline cic:/CoRN/algebra/CFields/f_rcpcl.con.
+inline "cic:/CoRN/algebra/CFields/f_rcpcl.con".
 
 (* UNEXPORTED
 Implicit Arguments f_rcpcl [F].
@@ -141,12 +143,16 @@ multiplication and the reciprocal. [x[/]y] is only defined if
 we have a proof of [y [#] Zero].
 *)
 
-inline cic:/CoRN/algebra/CFields/cf_div.con.
+inline "cic:/CoRN/algebra/CFields/cf_div.con".
 
 (* UNEXPORTED
 Implicit Arguments cf_div [F].
 *)
 
+(* NOTATION
+Notation "x [/] y [//] Hy" := (cf_div x y Hy) (at level 80).
+*)
+
 (*#*
 %\begin{convention}\label{convention:div-form}%
 - Division in fields is a (type dependent) ternary function: [(cf_div x y Hy)] is denoted infix by [x [/] y [//] Hy].
@@ -179,21 +185,21 @@ write [e[/] (Snring n)] and [e[/]TwoNZ], [e[/]ThreeNZ] and so on.
 *)
 
 (* UNEXPORTED
-Section Field_axioms.
+Section Field_axioms
 *)
 
-inline cic:/CoRN/algebra/CFields/F.var.
+inline "cic:/CoRN/algebra/CFields/Field_axioms/F.var" "Field_axioms__".
 
-inline cic:/CoRN/algebra/CFields/CField_is_CField.con.
+inline "cic:/CoRN/algebra/CFields/CField_is_CField.con".
 
-inline cic:/CoRN/algebra/CFields/rcpcl_is_inverse.con.
+inline "cic:/CoRN/algebra/CFields/rcpcl_is_inverse.con".
 
 (* UNEXPORTED
-End Field_axioms.
+End Field_axioms
 *)
 
 (* UNEXPORTED
-Section Field_basics.
+Section Field_basics
 *)
 
 (*#* ** Field basics
@@ -201,20 +207,20 @@ Section Field_basics.
 %\end{convention}%
 *)
 
-inline cic:/CoRN/algebra/CFields/F.var.
+inline "cic:/CoRN/algebra/CFields/Field_basics/F.var" "Field_basics__".
 
-inline cic:/CoRN/algebra/CFields/rcpcl_is_inverse_unfolded.con.
+inline "cic:/CoRN/algebra/CFields/rcpcl_is_inverse_unfolded.con".
 
-inline cic:/CoRN/algebra/CFields/field_mult_inv.con.
+inline "cic:/CoRN/algebra/CFields/field_mult_inv.con".
 
 (* UNEXPORTED
 Hint Resolve field_mult_inv: algebra.
 *)
 
-inline cic:/CoRN/algebra/CFields/field_mult_inv_op.con.
+inline "cic:/CoRN/algebra/CFields/field_mult_inv_op.con".
 
 (* UNEXPORTED
-End Field_basics.
+End Field_basics
 *)
 
 (* UNEXPORTED
@@ -222,7 +228,7 @@ Hint Resolve field_mult_inv field_mult_inv_op: algebra.
 *)
 
 (* UNEXPORTED
-Section Field_multiplication.
+Section Field_multiplication
 *)
 
 (*#*
@@ -231,44 +237,44 @@ Section Field_multiplication.
 %\end{convention}%
 *)
 
-inline cic:/CoRN/algebra/CFields/F.var.
+inline "cic:/CoRN/algebra/CFields/Field_multiplication/F.var" "Field_multiplication__".
 
-inline cic:/CoRN/algebra/CFields/mult_resp_ap_zero.con.
+inline "cic:/CoRN/algebra/CFields/mult_resp_ap_zero.con".
 
-inline cic:/CoRN/algebra/CFields/mult_lft_resp_ap.con.
+inline "cic:/CoRN/algebra/CFields/mult_lft_resp_ap.con".
 
-inline cic:/CoRN/algebra/CFields/mult_rht_resp_ap.con.
+inline "cic:/CoRN/algebra/CFields/mult_rht_resp_ap.con".
 
-inline cic:/CoRN/algebra/CFields/mult_resp_neq_zero.con.
+inline "cic:/CoRN/algebra/CFields/mult_resp_neq_zero.con".
 
-inline cic:/CoRN/algebra/CFields/mult_resp_neq.con.
+inline "cic:/CoRN/algebra/CFields/mult_resp_neq.con".
 
-inline cic:/CoRN/algebra/CFields/mult_eq_zero.con.
+inline "cic:/CoRN/algebra/CFields/mult_eq_zero.con".
 
-inline cic:/CoRN/algebra/CFields/mult_cancel_lft.con.
+inline "cic:/CoRN/algebra/CFields/mult_cancel_lft.con".
 
-inline cic:/CoRN/algebra/CFields/mult_cancel_rht.con.
+inline "cic:/CoRN/algebra/CFields/mult_cancel_rht.con".
 
-inline cic:/CoRN/algebra/CFields/square_eq_aux.con.
+inline "cic:/CoRN/algebra/CFields/square_eq_aux.con".
 
-inline cic:/CoRN/algebra/CFields/square_eq_weak.con.
+inline "cic:/CoRN/algebra/CFields/square_eq_weak.con".
 
-inline cic:/CoRN/algebra/CFields/cond_square_eq.con.
+inline "cic:/CoRN/algebra/CFields/cond_square_eq.con".
 
 (* UNEXPORTED
-End Field_multiplication.
+End Field_multiplication
 *)
 
 (* UNEXPORTED
-Section x_square.
+Section x_square
 *)
 
-inline cic:/CoRN/algebra/CFields/x_xminone.con.
+inline "cic:/CoRN/algebra/CFields/x_xminone.con".
 
-inline cic:/CoRN/algebra/CFields/square_id.con.
+inline "cic:/CoRN/algebra/CFields/square_id.con".
 
 (* UNEXPORTED
-End x_square.
+End x_square
 *)
 
 (* UNEXPORTED
@@ -276,7 +282,7 @@ Hint Resolve mult_resp_ap_zero: algebra.
 *)
 
 (* UNEXPORTED
-Section Rcpcl_properties.
+Section Rcpcl_properties
 *)
 
 (*#*
@@ -285,24 +291,24 @@ Section Rcpcl_properties.
 %\end{convention}%
 *)
 
-inline cic:/CoRN/algebra/CFields/F.var.
+inline "cic:/CoRN/algebra/CFields/Rcpcl_properties/F.var" "Rcpcl_properties__".
 
-inline cic:/CoRN/algebra/CFields/inv_one.con.
+inline "cic:/CoRN/algebra/CFields/inv_one.con".
 
-inline cic:/CoRN/algebra/CFields/f_rcpcl_wd.con.
+inline "cic:/CoRN/algebra/CFields/f_rcpcl_wd.con".
 
-inline cic:/CoRN/algebra/CFields/f_rcpcl_mult.con.
+inline "cic:/CoRN/algebra/CFields/f_rcpcl_mult.con".
 
-inline cic:/CoRN/algebra/CFields/f_rcpcl_resp_ap_zero.con.
+inline "cic:/CoRN/algebra/CFields/f_rcpcl_resp_ap_zero.con".
 
-inline cic:/CoRN/algebra/CFields/f_rcpcl_f_rcpcl.con.
+inline "cic:/CoRN/algebra/CFields/f_rcpcl_f_rcpcl.con".
 
 (* UNEXPORTED
-End Rcpcl_properties.
+End Rcpcl_properties
 *)
 
 (* UNEXPORTED
-Section MultipGroup.
+Section MultipGroup
 *)
 
 (*#*
@@ -311,26 +317,26 @@ Section MultipGroup.
 %\end{convention}%
 *)
 
-inline cic:/CoRN/algebra/CFields/F.var.
+inline "cic:/CoRN/algebra/CFields/MultipGroup/F.var" "MultipGroup__".
 
 (*#*
 The multiplicative monoid of NonZeros.
 *)
 
-inline cic:/CoRN/algebra/CFields/NonZeroMonoid.con.
+inline "cic:/CoRN/algebra/CFields/NonZeroMonoid.con".
 
-inline cic:/CoRN/algebra/CFields/fmg_cs_inv.con.
+inline "cic:/CoRN/algebra/CFields/fmg_cs_inv.con".
 
-inline cic:/CoRN/algebra/CFields/plus_nonzeros_eq_mult_dom.con.
+inline "cic:/CoRN/algebra/CFields/plus_nonzeros_eq_mult_dom.con".
 
-inline cic:/CoRN/algebra/CFields/cfield_to_mult_cgroup.con.
+inline "cic:/CoRN/algebra/CFields/cfield_to_mult_cgroup.con".
 
 (* UNEXPORTED
-End MultipGroup.
+End MultipGroup
 *)
 
 (* UNEXPORTED
-Section Div_properties.
+Section Div_properties
 *)
 
 (*#*
@@ -344,40 +350,40 @@ In the names of lemmas, we denote [[/]] by [div], and
 %\end{nameconvention}%
 *)
 
-inline cic:/CoRN/algebra/CFields/F.var.
+inline "cic:/CoRN/algebra/CFields/Div_properties/F.var" "Div_properties__".
 
-inline cic:/CoRN/algebra/CFields/div_prop.con.
+inline "cic:/CoRN/algebra/CFields/div_prop.con".
 
-inline cic:/CoRN/algebra/CFields/div_1.con.
+inline "cic:/CoRN/algebra/CFields/div_1.con".
 
-inline cic:/CoRN/algebra/CFields/div_1'.con.
+inline "cic:/CoRN/algebra/CFields/div_1'.con".
 
-inline cic:/CoRN/algebra/CFields/div_1''.con.
+inline "cic:/CoRN/algebra/CFields/div_1''.con".
 
 (* UNEXPORTED
 Hint Resolve div_1: algebra.
 *)
 
-inline cic:/CoRN/algebra/CFields/x_div_x.con.
+inline "cic:/CoRN/algebra/CFields/x_div_x.con".
 
 (* UNEXPORTED
 Hint Resolve x_div_x: algebra.
 *)
 
-inline cic:/CoRN/algebra/CFields/x_div_one.con.
+inline "cic:/CoRN/algebra/CFields/x_div_one.con".
 
 (*#*
 The next lemma says $x\cdot\frac{y}{z} = \frac{x\cdot y}{z}$
 #x.(y/z) = (x.y)/z#.
 *)
 
-inline cic:/CoRN/algebra/CFields/x_mult_y_div_z.con.
+inline "cic:/CoRN/algebra/CFields/x_mult_y_div_z.con".
 
 (* UNEXPORTED
 Hint Resolve x_mult_y_div_z: algebra.
 *)
 
-inline cic:/CoRN/algebra/CFields/div_wd.con.
+inline "cic:/CoRN/algebra/CFields/div_wd.con".
 
 (* UNEXPORTED
 Hint Resolve div_wd: algebra_c.
@@ -388,42 +394,42 @@ The next lemma says $\frac{\frac{x}{y}}{z} = \frac{x}{y\cdot z}$
 #[(x/y)/z = x/(y.z)]#
 *)
 
-inline cic:/CoRN/algebra/CFields/div_div.con.
+inline "cic:/CoRN/algebra/CFields/div_div.con".
 
-inline cic:/CoRN/algebra/CFields/div_resp_ap_zero_rev.con.
+inline "cic:/CoRN/algebra/CFields/div_resp_ap_zero_rev.con".
 
-inline cic:/CoRN/algebra/CFields/div_resp_ap_zero.con.
+inline "cic:/CoRN/algebra/CFields/div_resp_ap_zero.con".
 
 (*#*
 The next lemma says $\frac{x}{\frac{y}{z}} = \frac{x\cdot z}{y}$
 #[x/(y/z) = (x.z)/y]#
 *)
 
-inline cic:/CoRN/algebra/CFields/div_div2.con.
+inline "cic:/CoRN/algebra/CFields/div_div2.con".
 
 (*#*
 The next lemma says $\frac{x\cdot p}{y\cdot q} = \frac{x}{y}\cdot \frac{p}{q}$
 #[(x.p)/(y.q) = (x/y).(p/q)]#
 *)
 
-inline cic:/CoRN/algebra/CFields/mult_of_divs.con.
+inline "cic:/CoRN/algebra/CFields/mult_of_divs.con".
 
-inline cic:/CoRN/algebra/CFields/div_dist.con.
+inline "cic:/CoRN/algebra/CFields/div_dist.con".
 
-inline cic:/CoRN/algebra/CFields/div_dist'.con.
+inline "cic:/CoRN/algebra/CFields/div_dist'.con".
 
-inline cic:/CoRN/algebra/CFields/div_semi_sym.con.
+inline "cic:/CoRN/algebra/CFields/div_semi_sym.con".
 
 (* UNEXPORTED
 Hint Resolve div_semi_sym: algebra.
 *)
 
-inline cic:/CoRN/algebra/CFields/eq_div.con.
+inline "cic:/CoRN/algebra/CFields/eq_div.con".
 
-inline cic:/CoRN/algebra/CFields/div_strext.con.
+inline "cic:/CoRN/algebra/CFields/div_strext.con".
 
 (* UNEXPORTED
-End Div_properties.
+End Div_properties
 *)
 
 (* UNEXPORTED
@@ -439,25 +445,25 @@ Hint Resolve div_1 div_1' div_1'' div_wd x_div_x x_div_one div_div div_div2
 *)
 
 (* UNEXPORTED
-Section Mult_Cancel_Ap_Zero.
+Section Mult_Cancel_Ap_Zero
 *)
 
-inline cic:/CoRN/algebra/CFields/F.var.
+inline "cic:/CoRN/algebra/CFields/Mult_Cancel_Ap_Zero/F.var" "Mult_Cancel_Ap_Zero__".
 
-inline cic:/CoRN/algebra/CFields/mult_cancel_ap_zero_lft.con.
+inline "cic:/CoRN/algebra/CFields/mult_cancel_ap_zero_lft.con".
 
-inline cic:/CoRN/algebra/CFields/mult_cancel_ap_zero_rht.con.
+inline "cic:/CoRN/algebra/CFields/mult_cancel_ap_zero_rht.con".
 
-inline cic:/CoRN/algebra/CFields/recip_ap_zero.con.
+inline "cic:/CoRN/algebra/CFields/recip_ap_zero.con".
 
-inline cic:/CoRN/algebra/CFields/recip_resp_ap.con.
+inline "cic:/CoRN/algebra/CFields/recip_resp_ap.con".
 
 (* UNEXPORTED
-End Mult_Cancel_Ap_Zero.
+End Mult_Cancel_Ap_Zero
 *)
 
 (* UNEXPORTED
-Section CField_Ops.
+Section CField_Ops
 *)
 
 (*#*
@@ -474,62 +480,62 @@ Let [X] be a Field and [F,G:(PartFunct X)] have domains respectively
 %\end{convention}%
 *)
 
-inline cic:/CoRN/algebra/CFields/X.var.
+inline "cic:/CoRN/algebra/CFields/CField_Ops/X.var" "CField_Ops__".
 
-inline cic:/CoRN/algebra/CFields/F.var.
+inline "cic:/CoRN/algebra/CFields/CField_Ops/F.var" "CField_Ops__".
 
-inline cic:/CoRN/algebra/CFields/G.var.
+inline "cic:/CoRN/algebra/CFields/CField_Ops/G.var" "CField_Ops__".
 
 (* begin hide *)
 
-inline cic:/CoRN/algebra/CFields/P.con.
+inline "cic:/CoRN/algebra/CFields/CField_Ops/P.con" "CField_Ops__".
 
-inline cic:/CoRN/algebra/CFields/Q.con.
+inline "cic:/CoRN/algebra/CFields/CField_Ops/Q.con" "CField_Ops__".
 
 (* end hide *)
 
 (* UNEXPORTED
-Section Part_Function_Recip.
+Section Part_Function_Recip
 *)
 
 (*#*
 Some auxiliary notions are helpful in defining the domain.
 *)
 
-inline cic:/CoRN/algebra/CFields/R.con.
+inline "cic:/CoRN/algebra/CFields/CField_Ops/Part_Function_Recip/R.con" "CField_Ops__Part_Function_Recip__".
 
-inline cic:/CoRN/algebra/CFields/Ext2R.con.
+inline "cic:/CoRN/algebra/CFields/CField_Ops/Part_Function_Recip/Ext2R.con" "CField_Ops__Part_Function_Recip__".
 
-inline cic:/CoRN/algebra/CFields/part_function_recip_strext.con.
+inline "cic:/CoRN/algebra/CFields/part_function_recip_strext.con".
 
-inline cic:/CoRN/algebra/CFields/part_function_recip_pred_wd.con.
+inline "cic:/CoRN/algebra/CFields/part_function_recip_pred_wd.con".
 
-inline cic:/CoRN/algebra/CFields/Frecip.con.
+inline "cic:/CoRN/algebra/CFields/Frecip.con".
 
 (* UNEXPORTED
-End Part_Function_Recip.
+End Part_Function_Recip
 *)
 
 (* UNEXPORTED
-Section Part_Function_Div.
+Section Part_Function_Div
 *)
 
 (*#*
 For division things work out almost in the same way.
 *)
 
-inline cic:/CoRN/algebra/CFields/R.con.
+inline "cic:/CoRN/algebra/CFields/CField_Ops/Part_Function_Div/R.con" "CField_Ops__Part_Function_Div__".
 
-inline cic:/CoRN/algebra/CFields/Ext2R.con.
+inline "cic:/CoRN/algebra/CFields/CField_Ops/Part_Function_Div/Ext2R.con" "CField_Ops__Part_Function_Div__".
 
-inline cic:/CoRN/algebra/CFields/part_function_div_strext.con.
+inline "cic:/CoRN/algebra/CFields/part_function_div_strext.con".
 
-inline cic:/CoRN/algebra/CFields/part_function_div_pred_wd.con.
+inline "cic:/CoRN/algebra/CFields/part_function_div_pred_wd.con".
 
-inline cic:/CoRN/algebra/CFields/Fdiv.con.
+inline "cic:/CoRN/algebra/CFields/Fdiv.con".
 
 (* UNEXPORTED
-End Part_Function_Div.
+End Part_Function_Div
 *)
 
 (*#*
@@ -537,30 +543,38 @@ End Part_Function_Div.
 %\end{convention}%
 *)
 
-inline cic:/CoRN/algebra/CFields/R.var.
+inline "cic:/CoRN/algebra/CFields/CField_Ops/R.var" "CField_Ops__".
 
-inline cic:/CoRN/algebra/CFields/included_FRecip.con.
+inline "cic:/CoRN/algebra/CFields/included_FRecip.con".
 
-inline cic:/CoRN/algebra/CFields/included_FRecip'.con.
+inline "cic:/CoRN/algebra/CFields/included_FRecip'.con".
 
-inline cic:/CoRN/algebra/CFields/included_FDiv.con.
+inline "cic:/CoRN/algebra/CFields/included_FDiv.con".
 
-inline cic:/CoRN/algebra/CFields/included_FDiv'.con.
+inline "cic:/CoRN/algebra/CFields/included_FDiv'.con".
 
-inline cic:/CoRN/algebra/CFields/included_FDiv''.con.
+inline "cic:/CoRN/algebra/CFields/included_FDiv''.con".
 
 (* UNEXPORTED
-End CField_Ops.
+End CField_Ops
 *)
 
 (* UNEXPORTED
 Implicit Arguments Frecip [X].
 *)
 
+(* NOTATION
+Notation "{1/} x" := (Frecip x) (at level 2, right associativity).
+*)
+
 (* UNEXPORTED
 Implicit Arguments Fdiv [X].
 *)
 
+(* NOTATION
+Infix "{/}" := Fdiv (at level 41, no associativity).
+*)
+
 (* UNEXPORTED
 Hint Resolve included_FRecip included_FDiv : included.
 *)