Re: [isabelle] cross product in Isabelle



Hi Lyj,

there isn't yet a formalization of the cross product of two vectors in
Isabelle/HOL. At least not in Multivariate_Analysis. But I'm also not
aware of any other formalization.

 - Johannes

Am Donnerstag, den 12.06.2014, 12:08 +0800 schrieb lyj238:
> Dear experts:
>    The cross product in Euclide-space is directly defined in the multivariate lib in Isabelle?
> 
> 
> regards!
> 
> 2014-06-12 
> 
> 
> 
> lyj238 






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