Ssreflect Users Discussion List

[Jónathan Heras <>]

Thanks for the quick answer.

Jónathan


El 12/09/11 17:59, Georges Gonthier escribió:
>    Indeed, this is not defined per se. Instead we provide a local complement (U 
> :\: V)%VS, as this is equivalent in the finite dimensional setting we use, and 
> somewhat easier to handle (because it does not involve the creation of a new, 
> dependent type). The parallel projection addv_pi2 V (U :\: V) can be used to 
> project U onto U :\: V when (V<= U)%VS. (Caveat: vector.v has relatively few 
> lemmas about these projections).
>
>      Georges
>
> -----Original Message-----
> From: Jónathan Heras []
> Sent: 12 September 2011 16:30
> To: ssreflect
> Subject: Quotient of vector spaces
>
> Does anyone know if the definition of quotient of vector spaces has been 
> defined in the current distribution of SSReflect?
>
> I was looking it, and I almost sure that it was not defined, but could anyone 
> confirm me that?
>
> Thank you in advance.
>
> Jónathan.