More coercions added in the algebraic hierarchy.

diff --git a/matita/dama/integration_algebras.ma b/matita/dama/integration_algebras.ma
index 639d7188c0217e959ee047c2c7acfcb528ee9e7f..2a25457662394d2c3f4d0d1339faa0002f48b7b5 100644 (file)
--- a/matita/dama/integration_algebras.ma
+++ b/matita/dama/integration_algebras.ma
@@ -373,6 +373,13 @@ record algebra (K: field) (V:vector_space K) : Type \def
 interpretation "Algebra product" 'times a b =
  (cic:/matita/integration_algebras/a_mult.con _ _ _ a b).
 
+definition ring_of_algebra ≝
+ λK.λV:vector_space K.λA:algebra ? V.
+  mk_ring V (a_mult ? ? A)
+   (a_ring ? ? ? (a_algebra_properties ? ? A)).
+
+coercion cic:/matita/integration_algebras/ring_of_algebra.con.
+
 record is_f_algebra (S:archimedean_riesz_space)
  (A:algebra (rs_ordered_field_ch0 (ars_riesz_space S)) S) : Prop
 \def 
@@ -385,7 +392,10 @@ record is_f_algebra (S:archimedean_riesz_space)
 }.
 
 record f_algebra : Type \def 
-{ fa_archimedean_riesz_space: archimedean_riesz_space;
-  fa_algebra: algebra ? fa_archimedean_riesz_space;
+{ fa_archimedean_riesz_space:> archimedean_riesz_space;
+  fa_algebra:> algebra ? fa_archimedean_riesz_space;
   fa_f_algebra_properties: is_f_algebra fa_archimedean_riesz_space fa_algebra
 }.
+
+(* to be proved; see footnote 2 in the paper by Spitters *)
+axiom symmetric_a_mult: ∀A:f_algebra. symmetric ? (a_mult ? ? A).