wip dual pair

Author: mkerjean

theories/evt.v

@@ -135,4 +135,15 @@ Lemma nbhsE_subproof : nbhs = nbhs_ entourage.
     nbhsE_subproof.
 HB.end.
 
-Definition dual {R : ringType} (E : lmodType R) := {scalar E}. 
+Definition dual {R : ringType} (E : lmodType R) : Type := {scalar E}.
+(* Check fun {R : ringType} (E : lmodType R) => dual E : ringType. *)
+
+
+HB.mixin Record hasDual (R : ringType) (E' : lmodType R) E of GRing.Lmodule R E :=  {
+ dual_pair : E -> E' -> R;
+ dual_pair_rlinear : forall x, scalar (dual_pair x);
+ dual_pair_llinear : forall x, scalar (dual_pair^~ x);
+ ipair : injective ( fun x =>  dual_pair^~ x)
+
+}.   
+