Ssreflect Users Discussion List

[(Emilio Jesús Gallego Arias)]

Hello Georges,

thank you very much for your help.

Georges Gonthier 
<>
 writes:

> There are actually two definitions of the Kronecker product in the
> mathcomp library, [...]

Indeed I remember seeing tprod some time ago while poking around, but I
had forgotten! It is a nice starting point, thanks.

> There is cleaner (and documented) definition by Peng Wang in the
> coqfinitgroup gforge repository, in coconut/mxutil.v - unfortunately
> it never got promoted to the library proper - which might perhaps work
> better for you.

Unfortunately the coqfinitgroup repository is private, so I cannot
download mxutil.v, I would really appreciate if someone could share it
with me.

Thanks & best regards,
Emilio