`BookProof.NsPartialFourier.fourier_postcompCLM_apply` [CompleteSpace F] [CompleteSpace G] (T : F →L[ℂ] G) (f : 𝓢(V, F)) (x : V) : (𝓕 (postcompCLM T f) : 𝓢(V, G)) x = T ((𝓕 f : 𝓢(V

Initializing...

`BookProof.NsPartialFourier.fourier_postcompCLM_apply` [CompleteSpace F] [CompleteSpace G] (T : F →L[ℂ] G) (f : 𝓢(V, F)) (x : V) : (𝓕 (postcompCLM T f) : 𝓢(V, G)) x = T ((𝓕 f : 𝓢(V · Prove2Me