Ssreflect Users Discussion List

[Laurent Théry <>]

On 05/03/2012 01:15 PM, Laurent Théry wrote:
> On 05/03/2012 01:09 PM, Vincent Siles wrote:
> > In particular, how do we write "let f be a homomorphism from V1 to
> > V2". If I understand correctly, we can
> > only specify the underlying vectType, but not the vector spaces :
> >
> > Variable K : fieldType.
> > Variable V : vectType K.
> > Variable V1 V2 : {vector V}.
> >
> > Variable f : 'Hom(V,V).
> >
> > How do we say "f is from V1 to V2" ?
>
> Maybe you can just use the fact that the image of V1 is V2
>
> --
> Laurent