Ssreflect Users Discussion List

[Laurent Théry <>]

> The alternative is to do like in school and stay in vector
>
> Variables (K : fieldType) (vT : vectType K) (U V : {vspace vT}).
>
> Definition f x :=
>   \sum_(i < \dim U) coord (vbasis U) i x *: (vbasis V)`_i.
>
> and use  (linfun f).
Opps I am wrong this is not so simple, so maybe Cyril solution is a more 
direct one.

--
Laurent