Notation is finally fully working everywhere.

[helm.git] / matita / dama / fields.ma

diff --git a/matita/dama/fields.ma b/matita/dama/fields.ma
index 305c49764e9b651f368171ce00db323b29568956..5ab17edae98c7e2eafd4a3a94e65125ab9e7c433 100644 (file)
--- 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.