ssreflect - [ssreflect] Tensor product

Subject: Ssreflect Users Discussion List

List archive

[ssreflect] Tensor product

From: (Emilio Jesús Gallego Arias)
To:
Subject: [ssreflect] Tensor product
Date: Mon, 28 Sep 2015 19:40:33 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None ; spf=None ; spf=None
Ironport-phdr: 9a23:FPjomBYJ5cB7Afcj1L7p+V7/LSx+4OfEezUN459isYplN5qZpcq5bnLW6fgltlLVR4KTs6sC0LqK9f29EjVZut6oizMrTt9lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUiv2OQc9HOnpAIma153xjLDuvcCOKFwR33KUWvBbElaflU3prM4YgI9veO4a6yDihT92QdlQ3n5iPlmJnhzxtY+a9Z9n9DlM6bp6r5YTGfayQ6NtVqdCAToiPmspzMjwr1zCSxGO7z0dVH8Xm1xGGVvr9hb/C5j4ti/3ue1V0zObe8DwVrUsHzq4p+dGTR7siSBPFTMiYnqfpcV0iK9Up1qIvR122M+HM8muKPNic/aFLpshTm1bU5MJWg==
Organization: CRI ParisTech

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

[ssreflect] Tensor product, Emilio Jesús Gallego Arias, 09/28/2015
- RE: [ssreflect] Tensor product, Georges Gonthier, 09/29/2015
  - Re: [ssreflect] Tensor product, Emilio Jesús Gallego Arias, 09/29/2015

List archive

[ssreflect] Tensor product