X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matita%2Fdama%2Ffields.ma;h=5ab17edae98c7e2eafd4a3a94e65125ab9e7c433;hb=9ff984b29ac963eef2f79521ce9dd7cbb9ae2c59;hp=2aac4f446faa08237fe5ca25265e51630de0b147;hpb=92682f04ee34e7fb98ee5311646aaa62838f1e17;p=helm.git

diff --git a/matita/dama/fields.ma b/matita/dama/fields.ma
index 2aac4f446..5ab17edae 100644
--- a/matita/dama/fields.ma
+++ b/matita/dama/fields.ma
@@ -21,7 +21,7 @@ record is_field (R:ring) (inv:∀x:R.x ≠ 0 → R) : Prop
  {  (* multiplicative abelian properties *)
     mult_comm_: symmetric ? (mult R);
     (* multiplicative group properties *)
-    inv_inverse_: ∀x.∀p: x ≠ 0. mult ? (inv x p) x = 1
+    inv_inverse_: ∀x.∀p: x ≠ 0. inv x p * x = 1
  }.
 
 lemma opp_opp: ∀R:ring. ∀x:R. --x=x.
@@ -55,5 +55,6 @@ theorem inv_inverse: ∀F:field.∀x:F.∀p: x ≠ 0. (inv ? x p)*x = 1.
  apply (inv_inverse_ ? ? (field_properties F)).
 qed.
 
+(*CSC: qua funzionava anche mettendo ? al posto della prima F*)
 definition sum_field ≝
- λF:field. sum ? (plus F) 0 1.
+ λF:field. sum F (plus F) 0 1.