Smooth diagonal pullback of continuous multilinear maps

Mathlib bundles multilinear pullback as the continuous multilinear operator ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear. Applying the same continuous linear map in every input slot gives an operator-valued function that is smooth at every order, including the analytic order ω.

theorem ContinuousMultilinearMap.contDiff_compContinuousLinearMapContinuousMultilinear_diagonal {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {ι : Type u_5} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [Fintype ι] (n : WithTop ℕ∞) : ContDiff 𝕜 n fun (f : E →L[𝕜] F) => (compContinuousLinearMapContinuousMultilinear 𝕜 (fun (x : ι) => E) (fun (x : ι) => F) G) fun (x : ι) => f

Pulling back continuous multilinear maps along the same continuous linear map in every input slot is smooth as an operator-valued function, at every order including ω.