ssreflect - Re: [ssreflect] Mathematical Components for Quantum Computing

Subject: Ssreflect Users Discussion List

List archive

Re: [ssreflect] Mathematical Components for Quantum Computing

From: (Emilio Jesús Gallego Arias)
To: Robert Rand <>
Cc: Ssreflect-mailinglist <>
Subject: Re: [ssreflect] Mathematical Components for Quantum Computing
Date: Wed, 13 Sep 2017 21:21:31 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None ; spf=Pass ; spf=Pass
Ironport-phdr: 9a23:DExT7x+NJ5mpqP9uRHKM819IXTAuvvDOBiVQ1KB+2uIcTK2v8tzYMVDF4r011RmSAtWdtqoMotGVmp6jcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47WLmffqXyq7DMUBg63dU8sfry0ScbuiJGN0Oq/4YGbWQxOiHLpe6l7KhmetgjYrY8LmYZkLOA8xgaf8VVSfOEDyEt4dQrVmAzzroed+Z9n8iMYmf86ZdUIfqz+e6k3SvRxFjUvKCFmt4XQqRDfQF7XtTMnWWIMn08NWlCd4Q==
Organization: X80 Heavy Industries

Robert Rand
<>
writes:

> I think your postscript is misunderstanding something. I'm not looking to
> instantiate matrices *as* a field (which they aren't), I'm looking to
> define the conjugate transpose on `'M[C]`s where C is a numClosedFieldType.
> It sounds from Cyril as though this is possible in the development version
> of MathComp.

Oh, sorry, I see; indeed that is easy enough:

Variables (n : nat) (C : numClosedFieldType).
Implicit Types (A : 'M[C]_n).

Definition conj_mx A := trmx (map_mx conjC A).

etc... [

E.

[ssreflect] Mathematical Components for Quantum Computing, Robert Rand, 09/12/2017
- Re: [ssreflect] Mathematical Components for Quantum Computing, Laurent Thery, 09/12/2017
- Re: [ssreflect] Mathematical Components for Quantum Computing, Cyril, 09/12/2017
  - Re: [ssreflect] Mathematical Components for Quantum Computing, Bas Spitters, 09/12/2017
    - Re: [ssreflect] Mathematical Components for Quantum Computing, Robert Rand, 09/12/2017
  - Re: [ssreflect] Mathematical Components for Quantum Computing, Emilio Jesús Gallego Arias, 09/13/2017
    - Re: [ssreflect] Mathematical Components for Quantum Computing, Robert Rand, 09/13/2017
      - Re: [ssreflect] Mathematical Components for Quantum Computing, Emilio Jesús Gallego Arias, 09/13/2017

List archive

Re: [ssreflect] Mathematical Components for Quantum Computing