# Re: [isabelle] cross product in Isabelle

```Hi Lyj,

As Johannes says, there is no cross product formalized in
Multivariate_Analysis. But you can easily define one yourself, like
this:

theory Cross imports Multivariate_Analysis begin

definition cross2 :: "real × real ⇒ real × real ⇒ real" where
"cross2 = (λ(a1,a2). λ(b1,b2). a1 * b2 - a2 * b1)"

definition cross3 :: "real × real × real ⇒ real × real × real ⇒ real ×
real × real" where
"cross3 = (λ(a1,a2,a3). λ(b1,b2,b3). (a2 * b3 - a3 * b2, a3 * b1 -
a1 * b3, a1 * b2 - a2 * b1))"

It is then a simple matter to prove that the cross product is a
bounded bilinear operator. By interpreting the "bounded_bilinear"
locale you can obtain many useful lemmas automatically.

lemma bounded_bilinear_cross3: "bounded_bilinear cross3"
apply (rule bilinear_conv_bounded_bilinear [THEN iffD1])
apply (auto simp add: bilinear_def cross_def algebra_simps intro!: linearI)
done

interpretation cross: bounded_bilinear cross3
by (rule bounded_bilinear_cross3)

print_theorems (* this shows lemmas about distributivity, continuity,
limits, etc. *)

Hope this helps,
- Brian

On Thu, Jun 12, 2014 at 11:13 AM, Johannes Hölzl <hoelzl at in.tum.de> wrote:
> 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.