Subject: Ssreflect Users Discussion List
List archive
- From: Laurent Théry <>
- To: Vincent Siles <>
- Cc: Anders <>,
- Subject: Re: Bijection of vector spaces
- Date: Thu, 03 May 2012 13:29:56 +0200
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" ?
Best,
Vincent
More generally as vectro is a wrapper on top of mxalgebra.
To define a new notions you can either use the underlying matrix operations
or directly code your property with the notion from vectors.
Of course the first method is nice if there is in mxalgebra lots of material that can just lift.
Personnally in your case, I would favour the second case and define isomorphism as having
the same dimension and derive all the reflection lemmas that follow from this
definition (for example having an injective linear application sending V1 to V2).
--
Laurent
- Bijection of vector spaces, Anders, 05/02/2012
- Re: Bijection of vector spaces, Vincent Siles, 05/03/2012
- Message not available
- Re: Bijection of vector spaces, Laurent Théry, 05/03/2012
- Message not available
- Re: Bijection of vector spaces, Laurent Théry, 05/03/2012
- Re: Bijection of vector spaces, Vincent Siles, 05/03/2012
- Re: Bijection of vector spaces, Cyril Cohen, 05/03/2012
- Re: Bijection of vector spaces, Laurent Théry, 05/03/2012
- Re: Bijection of vector spaces, Laurent Théry, 05/03/2012
- Re: Bijection of vector spaces, Laurent Théry, 05/03/2012
- RE: Bijection of vector spaces, Georges Gonthier, 05/03/2012
- Re: Bijection of vector spaces, Laurent Théry, 05/03/2012
- RE: Bijection of vector spaces, Georges Gonthier, 05/03/2012
- Re: Bijection of vector spaces, Laurent Théry, 05/03/2012
- Re: Bijection of vector spaces, Laurent Théry, 05/03/2012
- Re: Bijection of vector spaces, Laurent Théry, 05/03/2012
Archive powered by MHonArc 2.6.18.