Re: [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.