Differentiability of bounded multilinear maps ?

Stream: Is there code for X?

[Sophie Morel]

It's all in the title: does mathlib know that bounded multilinear maps (in the sense of https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/NormedSpace/Multilinear.html#MultilinearMap.continuous_of_bound) are infinitely differentiable ? The closest I could find is the result for bounded bilinear maps, in https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Calculus/ContDiff/Basic.html#IsBoundedBilinearMap.contDiff.

(Context: I am still trying to define the Plücker map. I have the dimension formula for exterior powers, which allowed me to define the Plücker map as a map between types, but to prove that it is differentiable I will need something like "the canonical $r$-linear alternating map from $M$ to its $r$-exterior power is differentiable", and of course I will know that is bounded because I will choose a norm on exterior powers that makes this true.)

[Oliver Nash]

I don't think we have this. I recall wanting it for the Sphere Eversion project more than a year ago (where the multilinear map was also morally the determinant) but I somehow avoided needing it (probably by choosing coordinates).

[Sophie Morel]

Oh dear, I'm in possibly infinite dimension. (No coordinates for me !) I guess I can add that to my ever-growing todo list. Hopefully the proof for bounded bilinear maps is not too hard to adapt.