Directional differentiation and linear maps on Schwartz space

Applying a continuous real-linear map to the values of a Schwartz function commutes with directional differentiation. In particular, real and imaginary parts, and the embedding of real-valued functions into complex Schwartz space, commute with differentiation.

@[simp]

theorem TauCeti.lineDerivOp_postcompCLM {E : Type u_1} {F : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (v : E) (L : F →L[ℝ] G) (φ : SchwartzMap E F) : LineDeriv.lineDerivOp v ((SchwartzMap.postcompCLM L) φ) = (SchwartzMap.postcompCLM L) (LineDeriv.lineDerivOp v φ)

Directional differentiation commutes with a continuous real-linear map on the values of a Schwartz function.