Ssreflect Users Discussion List

[Cyril Cohen <>]

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