Ssreflect Users Discussion List

[Laurent Théry <>]

On 05/03/2012 04:32 PM, Georges Gonthier wrote:
>     That may be true, but as the library stands it'll be very difficult to 
> exploit that fact. For example, f^-1 will not cancel f.
> Cyril's suggestion produces an automorphism of the whole type, that maps V1 
> onto V2 if they have the same dimension.
> mxalgebra also supplies a somewhat complementary construction, which allows 
> to extend a given locally injective function to
> a global automorphism.
Yep if you need explicitly the automorphism while staying at the level 
of vector, you need to consider
the bases of the full space ((vbasis U) ++ (vbasis U^C)) and ((vbasis V) 
++ (vbasis V^C)).

--
Laurent