# Re: [isabelle] Vector transpose

*To*: Omar Jasim <oajasim1 at sheffield.ac.uk>
*Subject*: Re: [isabelle] Vector transpose
*From*: "Thiemann, Rene" <Rene.Thiemann at uibk.ac.at>
*Date*: Tue, 27 Feb 2018 10:56:42 +0000
*Accept-language*: de-DE, de-AT, en-US
*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>
*In-reply-to*: <CAAi=ges=qAOTHHMFO3Tz2viX6eBKY_zKPKVQ6RWpGLwE+0AS1g@mail.gmail.com>
*References*: <CAAi=ges=qAOTHHMFO3Tz2viX6eBKY_zKPKVQ6RWpGLwE+0AS1g@mail.gmail.com>
*Thread-index*: AQHTr7jbFnBBfJTrD0CU5Wq0JZLZ6KO4AxcA
*Thread-topic*: [isabelle] Vector transpose

Dear Omar,
if you’re not working with “real^’a” but with “real mat” from AFP/Jordan_Normal_Form/Matrix,
then you find “transpose_mat”. However, there “norm” is not defined.
However, using AFP/Perron_Frobenius/HMA_Connect you might easily be able to define transpose for “real^’a”
and then reuse the results for transpose_mat via the transfer-package.
For instance, eigen_vectors for “real^’a^’a” are defined like this, and results are just transferred.
Cheers,
René
> I was looking for a transpose of a vector (real^'a) but I couldn't find it.
> Probably there is no such definition. The problem I faced is:
>
> lemma
> fixes E :: "(real, 6) vec"
> and Q :: "((real, 6) vec, 6) vec"
> and B:: "((real, 3) vec, 6) vec"
> shows "norm((E v* Q) v* B) = norm(transpose (B) *v (Q*v E))"
>
> So please, is there a transpose of a vector defined in Isabelle/HOL?

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*