Ssreflect Users Discussion List

[Georges Gonthier <>]

   Hello Emilio,
  There are actually two definitions of the Kronecker product in the mathcomp 
library, though neither is documented: one in file mxtens.v, and one in 
character.v (the latter as an auxiliary to the construction of character 
products). Also, both definitions are somewhat inelegant. 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.
   Best,
Georges

-----Original Message-----
From: 

 
[mailto:]
 On Behalf Of Emilio Jesús Gallego Arias
Sent: 28 September 2015 18:41
To: 

Subject: [ssreflect] Tensor product

Dear ssr/mathcomp devs,

is there any existing work in formalizing tensor products for vector 
spaces/linear maps?

In particular, I need a few basic facts about Kroenecker products.

I can think of a few ways of doing it using mathcomp; any 
suggestion/advice/key piece of the library would be very welcome of course.

Thanks and best regards,
Emilio