From 518447fcf71d1e8e4e63f7498771a0d13a2d1446 Mon Sep 17 00:00:00 2001
From: Enrico Zoli <??>
Date: Tue, 24 Oct 2006 16:03:12 +0000
Subject: [PATCH] More coercions added in the algebraic hierarchy.

---
 matita/dama/integration_algebras.ma | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

diff --git a/matita/dama/integration_algebras.ma b/matita/dama/integration_algebras.ma
index 639d7188c..2a2545766 100644
--- 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).
-- 
2.39.2