Theorem: SchwartzMap.integralCLM_smul_apply (ForML/SchwartzLp.lean)

State before:
E : Type u_1
F : Type u_2
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : NormedSpace ℝ E
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℝ F
mE : MeasureSpace E
inst✝⁹ : FiniteDimensional ℝ E
inst✝⁸ : BorelSpace E
inst✝⁷ : Measure.IsAddHaarMeasure volume
𝕜✝ : Type u_3
𝕜' : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜✝
inst✝⁵ : CompleteSpace F
inst✝⁴ : NormedSpace 𝕜✝ F
inst✝³ : SMulCommClass ℝ 𝕜✝ F
𝕜 : Type u_5
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
c : 𝕜
f : 𝓢(E, F)
⊢ integralCLM (c • f) = c • integralCLM f
Tactic:
simp [integralCLM_apply, integral_smul]
State after:
no goals