Ssreflect Users Discussion List

[Vincent Siles <>]

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" ?

Best,
Vincent

2012/5/2 Anders <>:
> Hello,
>
> What is the syntax for defining a bijection between two vector spaces?
>
> Our goal is to prove that two vector spaces of the same dimension are
> isomorphic. Any suggestions are welcome.
>
> Best regards,
> Anders