Ssreflect Users Discussion List

[Cyril <>]

Hi,

On 12/09/2017 00:32, Robert Rand wrote:
> I 
> don't know if there's any definition of conjugate transpose for matrices 
> containing closedFieldTypes. (I've been able to define conj_trmx for 
> 'M[algC] - unfortunately, closedFieldType doesn't seem to have an 
> associate conjugate operation?) We would then need some algebraic 
> identities involving conjugate transpose and Kronecker products, plus 
> the basic quantum matrices.

There is an upcomming generalization of numClosedFieldTypes (available 
only in the development version until now, but soon to be released) that 
contains conjugation.
I used it in a development to prove the spectral theorem for normal 
operators: 
https://github.com/CohenCyril/spectral/blob/master/theories/spectral.v

Best,
--
Cyril