Theorem: SchwartzMap.integralCLM_neg_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
f : 𝓢(E, F)
⊢ integralCLM (-f) = -integralCLM f
Tactic:
rw [ContinuousLinearMap.map_neg]
State after:
no goals