Subject: Ssreflect Users Discussion List
List archive
- From: AffeldtReynald <>
- To: Ssreflect <>, Pierre-Yves Strub <>
- Subject: Re: [ssreflect] coconut/mxutil.v ?
- Date: Thu, 11 Feb 2021 10:36:15 +0000
- Accept-language: en-US
- Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=aist.go.jp; dmarc=pass action=none header.from=aist.go.jp; dkim=pass header.d=aist.go.jp; arc=none
- Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-SenderADCheck; bh=OM+pCoPeJBmVWWwdEQPbFwvmbFwR37Xeo9VoJxdtqPk=; b=cdc79Jl8id0sBkIztOWURmitJRoqP076goJXf90wXS7f35kpoQ7gnUl/xKCCThSJiOxVFZRE/1ZoRFgUzauAVhVfPP5z2FvI3DGd/9pJn1tyq5a4EOz85zFMzuI7WqOvLBIErAe8S/wHM1AGGzHkFgB+FfHI9bIvFES7ZOv0lQQA3e/2+yOqMFjSMBw8R/QOfC6GevxdU0fFIlMNqjBmIU7xENSxHBJoQYEedFJktLCuRspZHr9r8GoUAlbvbE4rDPJJSmCbiDRe5vG363Xi2bpDZbG2c6YjpTVW/8bst7wdXgXpAMQWYWByRSOUTADX/Me+AYT/zJ1UvL4qJ9U2ug==
- Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=mrkRv4ASpoUTFeyO6E6A/GK0sQnndWC+uvFMFijpUBBcgFFpm9sH3e/ikclWAuoftXkbzhNkdDOr3P9cHUazMEq9vDb8Ww62HSvIiq+zOIiVd3zOg8SbDYKjgxDl8M3L7mlRFOuA9BnkiltrC6dQqycBA/gRc/zdz4PCYw09xKaGd+aTBcjngv2ArdFEGqB6njDz3Qx3NnCMY6GPPINbxjXQ90mxwG/OxlSOzDr0MR0RmrkJcNLC+q1Q9AknrFuHUrmfBueU9Qc2fFdEQZWtbuPJebw09ha6QaE3nnqG360hD+DQClULWFo1zm6onJyIAUnohe/GMSVc/AbwXtba+w==
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None ; spf=Pass ; spf=Pass
- Ironport-phdr: 9a23:JyZ/uBKongCCMBIfuNmcpTZWNBhigK39O0sv0rFitYgXKvX/rarrMEGX3/hxlliBBdydt6sVzbeG+PG4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCe5bL9oLBi7rgrdu80KjYB/Nqs/1xzFr2dSde9L321oP1WTnxj95se04pFu9jlbtuwi+cBdT6j0Zrw0QrNEAjsoNWA1/9DrugLYTQST/HscU34ZnQRODgPY8Rz1RJbxsi/9tupgxCmXOND9QL4oVTi+6apgVQTlgzkbOTEn7G7Xi9RwjKNFrxKnuxx/2JPfbIWMOPZjYq/RYdYWSGxcVchTSiNBGJuxYYsRAeQcIeZWoYrzp1UMohu/GQaiC+zgxyRUhn/vwaE2z/gtHR3Y0AEmAtkAsG7UrNLwNKoKTe21wqfIwivHb/xLxTfz9JbHcxAnof6WWbJ/bNfaxE41FwzbjlSQr5bqPzeI2egXqWeb4eRgWvyri2E6twF8uSKgxsY3ionVnI4VxVfE+T97wIYtPNC1TlNwbtG4HpVKrS6aK5d2Td04Q2FuoCs2178LtYO/cSQW1JgpxwPSZvKDfoWH4hzuW/ucLDhkiH57Zb6yhxK//Fa9xuD/S8S5zFdHoyVZntXRq30A1xLe586aQfVz+Ueh3CyA1wHV6uxcLkA0lLbbK548wrErjJYcrUPDHirwlU7rj6GWbl0p9+e05+j9f7nqup2RO5VphgzxL6gigMOyDOQgPgQTX2WX5f6w2KPn8EHjXblHgfk7nrPHvJ3UK8kXvrC1Dg5J3ost7huzEiuq3dAZkHQCLV9JZB2Kgo3rNlzPJf31COqzjlqqnTx23f7JJKfhDY/ILnXbkLfuY7J960lExQQ3195R/45YBqwYLPzqR0H9qsXUDhgiPAOq2ernD8h91p8FVmKIH6+ZNr7dvUWQ5uI1JOmMeJEatyrhK/gk4P7ui2U1mVgAfam12ZsXb3e4Hvd8L0qFZnrsh88NEWYMvgUgUOznkFKPXSJJa3qvQ64x5Cs3BJ+pAIveXIygj7yM0D++HpJMZ2BGDl6MEW3vd4WBQ/oMcjydI89nkjMeUbiuVpUt2gugtA/01bVnKvfb+jEDuJ351dh1/PHTmQs99TxzFcid0XmNQ3lunmwUXz82wLx/oUtlx1eYyqh4meJXFdJX5/xXTgg6KYXRz/d6CtD3QgLOZM2FSFegQtW8ADE+VMg9w9EUYxU1J9L3tQvZ0iSuDrQJ3+iQH4Y5/KbR1GTZIt1njnfAzqgoyVggWMpGc2O80Oo3zwneHZTE1nSHmr3iTrgGwSSFoH+CwHCUsQRJTgNreb7ZR20VIE3L+4fX/ETHGpagB7kjPhd7xN+EI69GIonzgERATfPvft3QbW+1l3uYDBeT2vWDa8zoYzNOj23mFEEYnlVLrj69Pg8kC3Lk+jqGVWA8JRfUe0rptNJGhjajVEZtlVODblZ9kbWyvBwN16TFFqEjm4kcsSJkkA1aWVaw29WKVIiinyw5JeB7Wol4511Kk2XEqwZ6I5qsabh4gUITeBh2uEWo0AhrDoJHko4hq3Z4lVMje5Ld60tIcnaj5b61P7TWLmfo+xX2Mfzf20rCltmRvKUXuq01
Here you are:
https://github.com/wangpengmit/ssmatrix-theory
________________________________________
From: <> on behalf of
Pierre-Yves Strub <>
Sent: Thursday, February 11, 2021 5:51 PM
To: Ssreflect
Subject: [ssreflect] coconut/mxutil.v ?
Hi,
Some years ago (around September 2015), Georges mentioned a file
containing a clean & documented version of the Kronecker product in
mathcomp. The filename is "coconut/mxutil.v" and should be in the
coqfinitgroup repository. However, I am not able to find it in the
archived version of the coqfinitegroup repository. Does somebody know
where I could find it?
Best, Pierre-Yves.
- [ssreflect] coconut/mxutil.v ?, Pierre-Yves Strub, 02/11/2021
- Re: [ssreflect] coconut/mxutil.v ?, AffeldtReynald, 02/11/2021
Archive powered by MHonArc 2.6.19+.