exact continuous_mul
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
f : ℝ → F
hf : Integrable f
⊢ Continuous fun p => ((LinearMap.mul ℝ ℝ) p.1) p.2
no goals