pointwise curl operator in Mathlib?

Stream: Is there code for X?

[Ali Bekheet]

Is there a pointwise curl operator in Mathlib?

I'd like to contribute curl : ((Fin 3 → ℝ) → (Fin 3 → ℝ)) → (Fin 3 → ℝ) → (Fin 3 → ℝ) defined via fderiv and Pi.single, following the crossProduct pattern. I have a working draft with linearity lemmas. Is anyone else working on this, and would it be welcome?

[Eric Wieser]

Putnambench uses

    (curl : ((Fin 3 → ℝ) → (Fin 3 → ℝ)) → ((Fin 3 → ℝ) → (Fin 3 → ℝ)))
    (curl_def : ∀ f x, curl f x = ![
      fderiv ℝ f x (Pi.single 1 1) 2 - fderiv ℝ f x (Pi.single 2 1) 1,
      fderiv ℝ f x (Pi.single 2 1) 0 - fderiv ℝ f x (Pi.single 0 1) 2,
      fderiv ℝ f x (Pi.single 0 1) 1 - fderiv ℝ f x (Pi.single 1 1) 0])

[Eric Wieser]

PhysLean also has a definition

[Weiyi Wang]

I guess Mathlib would want a more generic definition?

[Eric Wieser]

I would guess it wants the differential form instead

[Eric Wieser]

(which I guess docs#extDeriv helps with)

[Yury G. Kudryashov]

I think that it makes sense to have the curl too. It should be possible to define it in an inner product space of dimension 3.