R_AbsRing -> R_Ring.

FEM/Finite_dim.v

@@ -6,9 +6,9 @@ From LM Require Import check_sub_structure.
 
 Section FD.
 
-Context {E : ModuleSpace R_AbsRing}.
-
+Context {E : ModuleSpace R_Ring}.
 
+(* Imposer que la "base B" est libre ? *)
 Record FiniteDim := FD {
   dim : nat ;
   B : nat -> E ;
@@ -73,7 +73,7 @@ rewrite scal_assoc; easy.
 Qed.
 
 
-(*Check (forall P: FiniteDim, Sg_ModuleSpace (toto P)).*)
+Check (forall P: FiniteDim, Sg_ModuleSpace (FiniteDim_compatible_m P)).
 
 End FD.
 
@@ -81,8 +81,8 @@ End FD.
 Section FD_bij.
 
 
-Context {E1 : ModuleSpace R_AbsRing}.
-Context {E2 : ModuleSpace R_AbsRing}.
+Context {E1 : ModuleSpace R_Ring}.
+Context {E2 : ModuleSpace R_Ring}.
 
 Variable F1: @FiniteDim E1.
 Variable F2: @FiniteDim E2.
@@ -90,6 +90,7 @@ Variable F2: @FiniteDim E2.
 Hypothesis F12_dim: dim F1 = dim F2.
 
 Definition F1_to_F2 : E1 -> E2.
+Proof.
 intros x.
 case (excluded_middle_informative (F1 x)); intros H.
 2: apply zero. (*not in F1 *)
@@ -110,6 +111,7 @@ exists L; easy.
 Qed.
 
 Definition F2_to_F1 : E2 -> E1.
+Proof.
 intros x.
 case (excluded_middle_informative (F2 x)); intros H.
 2: apply zero. (*not in F2 *)