`BookProof.MixedLinearEsa.momentumOp_apply` (m : V) (f : 𝓢(V, ℂ)) (x : V) : (momentumOp m f) x = (-Complex.I) * (fderiv ℝ f x m)

Initializing...

`BookProof.MixedLinearEsa.momentumOp_apply` (m : V) (f : 𝓢(V, ℂ)) (x : V) : (momentumOp m f) x = (-Complex.I) * (fderiv ℝ f x m) · Prove2Me