Ssreflect Users Discussion List

[Georges Gonthier <>]

  Dear Cyril,
I believe the function lin_mx (in matrix.v) is exactly what you want :-)
You are right, though, about the vector  library providing only limited 
support for converting from abstract vectors to line vectors and matrices.
This is in part due to the fact that such operations tend to get cluttered 
with the bases of the various subspaces considered, which can't be elided as 
easily in Coq as in non-formal math; thus one is somewhat better off with 
pure matrices with an implicit interpretation.

-- Georges

-----Original Message-----
From: Cyril Cohen [] 
Sent: 05 September 2012 19:21
To: 
Subject: matrix of an endomorphism

Dear ssreflect list,

Given (K : fieldType) and (n : nat), consider the function (fun A : 'M[K]_n 
=> A * B - B * A^T : 'M[K]_n) It is linear and thus I want to show it is an 
endomorphism, but as an endomorphism of 'rV_(n * n), i.e. a matrix of 'M_(n * 
n).

Of course, it is easy to build the endomorphism linfun (fun A : 'M[K]_n => A 
* B - B * A^T)) : 'End([vectType K of 'M_n]) but the only function I know 
would transform it into a matrix is the f2mx internal function, but I don't 
want to break the abstraction.

It seems there is no "matrix of an endomorphism in a given basis" function, 
which is so common in standard maths. I believe the "everything is a matrix" 
was a replacement from this standard notion, but how does it deal with the 
example above ? Did I miss something ? What did I miss ?

Best,
--
Cyril