X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Ffields.ma;h=305c49764e9b651f368171ce00db323b29568956;hb=f79585fe2f19c4a545938e189439d87b2611a47a;hp=0618f4923a92097fafcdd2199067bb4914679ccf;hpb=85fce74d6a0cd8e83e59895e81f1bc09d21ef4c2;p=helm.git

diff --git a/helm/software/matita/dama/fields.ma b/helm/software/matita/dama/fields.ma
index 0618f4923..305c49764 100644
--- a/helm/software/matita/dama/fields.ma
+++ b/helm/software/matita/dama/fields.ma
@@ -24,7 +24,7 @@ record is_field (R:ring) (inv:∀x:R.x ≠ 0 → R) : Prop
     inv_inverse_: ∀x.∀p: x ≠ 0. mult ? (inv x p) x = 1
  }.
 
-lemma opp_opp: \forall R:ring. \forall x:R. (-(-x))=x.
+lemma opp_opp: ∀R:ring. ∀x:R. --x=x.
 intros; 
 apply (cancellationlaw ? (-x) ? ?); 
 rewrite > (opp_inverse R x); 
@@ -50,10 +50,11 @@ theorem mult_comm: ∀F:field.symmetric ? (mult F).
  apply (mult_comm_ ? ? (field_properties F)).
 qed.
 
-theorem inv_inverse: ∀F:field.∀x.∀p: x ≠ 0. mult ? (inv F x p) x = 1.
+theorem inv_inverse: ∀F:field.∀x:F.∀p: x ≠ 0. (inv ? x p)*x = 1.
  intro;
  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) (zero F) (one F).
+ λF:field. sum F (plus F) 0 1.