Ssreflect Users Discussion List

[Laurent Théry <>]

On 05/03/2012 03:33 PM, Cyril Cohen wrote:
> Hi,
> it seems I sent my message to Anders only ...
>
> On 02/05/2012 17:10, Cyril Cohen wrote:
> > On 02/05/2012 15:23, Anders wrote:
> > > Our goal is to prove that two vector spaces of the same dimension are
> > > isomorphic. Any suggestions are welcome.
> > If by vector spaces you mean matrices, then I'd say that if your two vector
> > spaces are M and M', then ((row_ebase M)^-1 *m M') is your isomorphism (I 
> > think
> > that's true, but I didn't check).
> I think I was wrong and that the good isomorphism is in fact
> f = ((row_ebase M)^-1 *m (row_ebase M')).
> Because if the "gauss decompositions" of M and M' are M = C D R and M' = C' D 
> R'
> (where D is pid d, with d the common dimension).
> Then M f = C D R R^-1 R' = C D R' which represents the same vector space as 
> M'.
>
> > If you mean subspaces of a vectType, then I don't know a direct solution 
> > (which
> > doesn't break the abstraction layer provided by vector.v). But you could 
> > define
> > an 'End(vT) using the previous matrix construction, where M and M' are the 
> > vs2mx
> > of your two subspaces.
> I think this is kind of a lift Laurent was talking about ...
>
> Best,

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).