Theorem: F_add (PrimeNumberTheoremAnd/Fourier.lean)

State before:
f g : ℝ → ℂ
hf : Integrable f volume
hg : Integrable g volume
x : ℝ
⊢ Continuous fun p => ((innerₗ ℝ) p.1) p.2
Tactic:
exact continuous_mul
State after:
no goals